Theorem fiint 4534

Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite non-empty subcollection of A is in A." This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally.

Assertion

Ref	Expression
fiint	|- (A.x e. A A.y e. A (x i^i y) e. A <-> A.x((x (_ A /\ x =/= (/) /\ E.y e. om x ~~ y) -> |^|x e. A))

Distinct variable group:   x,y,A

Proof of Theorem fiint

Step	Hyp	Ref	Expression
1		breq1 2612	. . . . . . . . . . . . . . 15 |- (y = (/) -> (y ~~ x <-> (/) ~~ x))
2	1	anbi2d 614	. . . . . . . . . . . . . 14 |- (y = (/) -> (((x (_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x (_ A /\ x =/= (/)) /\ (/) ~~ x)))
3	2	imbi1d 611	. . . . . . . . . . . . 13 |- (y = (/) -> ((((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)))
4	3	albidv 1273	. . . . . . . . . . . 12 |- (y = (/) -> (A.x(((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)))
5		breq1 2612	. . . . . . . . . . . . . . 15 |- (y = v -> (y ~~ x <-> v ~~ x))
6	5	anbi2d 614	. . . . . . . . . . . . . 14 |- (y = v -> (((x (_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x (_ A /\ x =/= (/)) /\ v ~~ x)))
7	6	imbi1d 611	. . . . . . . . . . . . 13 |- (y = v -> ((((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)))
8	7	albidv 1273	. . . . . . . . . . . 12 |- (y = v -> (A.x(((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)))
9		breq1 2612	. . . . . . . . . . . . . . 15 |- (y = suc v -> (y ~~ x <-> suc v ~~ x))
10	9	anbi2d 614	. . . . . . . . . . . . . 14 |- (y = suc v -> (((x (_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x (_ A /\ x =/= (/)) /\ suc v ~~ x)))
11	10	imbi1d 611	. . . . . . . . . . . . 13 |- (y = suc v -> ((((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x (_ A /\ x =/= (/)) /\ suc v ~~ x) -> |^|x e. A)))
12	11	albidv 1273	. . . . . . . . . . . 12 |- (y = suc v -> (A.x(((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x (_ A /\ x =/= (/)) /\ suc v ~~ x) -> |^|x e. A)))
13		visset 1804	. . . . . . . . . . . . . . . . . . . 20 |- x e. V
14	13	ensym 4393	. . . . . . . . . . . . . . . . . . 19 |- ((/) ~~ x -> x ~~ (/))
15		en0 4404	. . . . . . . . . . . . . . . . . . 19 |- (x ~~ (/) <-> x = (/))
16	14, 15	sylib 198	. . . . . . . . . . . . . . . . . 18 |- ((/) ~~ x -> x = (/))
17	16	anim1i 334	. . . . . . . . . . . . . . . . 17 |- (((/) ~~ x /\ x =/= (/)) -> (x = (/) /\ x =/= (/)))
18	17	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((x =/= (/) /\ (/) ~~ x) -> (x = (/) /\ x =/= (/)))
19	18	adantll 392	. . . . . . . . . . . . . . 15 |- (((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> (x = (/) /\ x =/= (/)))
20		pm3.24 656	. . . . . . . . . . . . . . . . 17 |- -. (x = (/) /\ -. x = (/))
21	20	pm2.21i 77	. . . . . . . . . . . . . . . 16 |- ((x = (/) /\ -. x = (/)) -> |^|x e. A)
22		df-ne 1579	. . . . . . . . . . . . . . . 16 |- (x =/= (/) <-> -. x = (/))
23	21, 22	sylan2b 452	. . . . . . . . . . . . . . 15 |- ((x = (/) /\ x =/= (/)) -> |^|x e. A)
24	19, 23	syl 10	. . . . . . . . . . . . . 14 |- (((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)
25	24	ax-gen 960	. . . . . . . . . . . . 13 |- A.x(((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)
26	25	a1i 8	. . . . . . . . . . . 12 |- (A.z e. A A.w e. A (z i^i w) e. A -> A.x(((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A))
27		ax-17 968	. . . . . . . . . . . . . 14 |- (A.z e. A A.w e. A (z i^i w) e. A -> A.xA.z e. A A.w e. A (z i^i w) e. A)
28		hba1 1000	. . . . . . . . . . . . . 14 |- (A.x(((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> A.xA.x(((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A))
29		ssel 2053	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x (_ A -> ((f` v) e. x -> (f` v) e. A))
30		f1ofo 3680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-1-1-onto->x -> f:suc v-onto->x)
31		fof 3657	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-onto->x -> f:suc v-->x)
32		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- v e. V
33	32	sucid 3041	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- v e. suc v
34		ffvelrn 3799	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f:suc v-->x /\ v e. suc v) -> (f` v) e. x)
35	33, 34	mpan2 694	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-->x -> (f` v) e. x)
36	30, 31, 35	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc v-1-1-onto->x -> (f` v) e. x)
37	29, 36	syl5 21	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x (_ A -> (f:suc v-1-1-onto->x -> (f` v) e. A))
38	37	imp 350	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x (_ A /\ f:suc v-1-1-onto->x) -> (f` v) e. A)
39	38	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 |- (((x (_ A /\ f:suc v-1-1-onto->x) /\ (A.x(((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) /\ A.z e. A A.w e. A (z i^i w) e. A)) -> (f` v) e. A)
40		imassrn 3399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (f"v) (_ ran f
41		f1o2 3678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (f:suc v-1-1-onto->x <-> (f Fn suc v /\ Fun `'f /\ ran f = x))
42		3simp3 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((f Fn suc v /\ Fun `'f /\ ran f = x) -> ran f = x)
43	41, 42	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f:suc v-1-1-onto->x -> ran f = x)
44	43	sseq2d 2079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (f:suc v-1-1-onto->x -> ((f"v) (_ ran f <-> (f"v) (_ x))
45	40, 44	mpbii 193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1-onto->x -> (f"v) (_ x)
46		sstr2 2061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f"v) (_ x -> (x (_ A -> (f"v) (_ A))
47	45, 46	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:suc v-1-1-onto->x -> (x (_ A -> (f"v) (_ A))
48	47	anim1d 558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc v-1-1-onto->x -> ((x (_ A /\ (f"v) =/= (/)) -> ((f"v) (_ A /\ (f"v) =/= (/))))
49		f1of1 3673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:suc v-1-1-onto->x -> f:suc v-1-1->x)
50		sssucid 3037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- v (_ suc v
51		f1ores 3688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f:suc v-1-1->x /\ v (_ suc v) -> (f |` v):v-1-1-onto->(f"v))
52	50, 51	mpan2 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:suc v-1-1->x -> (f |` v):v-1-1-onto->(f"v))
53	32	f1oen 4379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f |` v):v-1-1-onto->(f"v) -> v ~~ (f"v))
54	49, 52, 53	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc v-1-1-onto->x -> v ~~ (f"v))
55	48, 54	jctird 600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f:suc v-1-1-onto->x -> ((x (_ A /\ (f"v) =/= (/)) -> (((f"v) (_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v))))
56		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- f e. V
57		imaexg 3400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f e. V -> (f"v) e. V)
58	56, 57	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f"v) e. V
59		sseq1 2072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> (x (_ A <-> (f"v) (_ A))
60		neeq1 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> (x =/= (/) <-> (f"v) =/= (/)))
61	59, 60	anbi12d 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"v) -> ((x (_ A /\ x =/= (/)) <-> ((f"v) (_ A /\ (f"v) =/= (/))))
62		breq2 2613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"v) -> (v ~~ x <-> v ~~ (f"v)))
63	61, 62	anbi12d 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x = (f"v) -> (((x (_ A /\ x =/= (/)) /\ v ~~ x) <-> (((f"v) (_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v))))
64		inteq 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"v) -> |^|x = |^|(f"v))
65	64	eleq1d 1532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x = (f"v) -> (|^|x e. A <-> |^|(f"v) e. A))
66	63, 65	imbi12d 624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (x = (f"v) -> ((((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) <-> ((((f"v) (_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v)) -> |^|(f"v) e. A)))
67	58, 66	cla4v 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A.x(((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> ((((f"v) (_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v)) -> |^|(f"