Theorem fiint 3445

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(s):   x,y,A

Proof of Theorem fiint

Step	Hyp	Ref	Expression
1		ineq1 1638	. . . . 5 |- (x = z -> (x i^i y) = (z i^i y))
2	1	eleq1d 1155	. . . 4 |- (x = z -> ((x i^i y) e. A <-> (z i^i y) e. A))
3	2	biraldv 1219	. . 3 |- (x = z -> (A.y e. A (x i^i y) e. A <-> A.y e. A (z i^i y) e. A))
4	3	cbvralv 1333	. 2 |- (A.x e. A A.y e. A (x i^i y) e. A <-> A.z e. A A.y e. A (z i^i y) e. A)
5		ineq2 1639	. . . . 5 |- (y = w -> (z i^i y) = (z i^i w))
6	5	eleq1d 1155	. . . 4 |- (y = w -> ((z i^i y) e. A <-> (z i^i w) e. A))
7	6	cbvralv 1333	. . 3 |- (A.y e. A (z i^i y) e. A <-> A.w e. A (z i^i w) e. A)
8	7	biral 1223	. 2 |- (A.z e. A A.y e. A (z i^i y) e. A <-> A.z e. A A.w e. A (z i^i w) e. A)
9		breq1 2065	. . . . . . . . . . . . . . 15 |- (y = (/) -> (y ~~ x <-> (/) ~~ x))
10	9	anbi2d 468	. . . . . . . . . . . . . 14 |- (y = (/) -> (((x (_ A /\ -. x = (/)) /\ y ~~ x) <-> ((x (_ A /\ -. x = (/)) /\ (/) ~~ x)))
11	10	imbi1d 465	. . . . . . . . . . . . 13 |- (y = (/) -> ((((x (_ A /\ -. x = (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x (_ A /\ -. x = (/)) /\ (/) ~~ x) -> |^|x e. A)))
12	11	bialdv 935	. . . . . . . . . . . 12 |- (y = (/) -> (A.x(((x (_ A /\ -. x = (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x (_ A /\ -. x = (/)) /\ (/) ~~ x) -> |^|x e. A)))
13		breq1 2065	. . . . . . . . . . . . . . 15 |- (y = v -> (y ~~ x <-> v ~~ x))
14	13	anbi2d 468	. . . . . . . . . . . . . 14 |- (y = v -> (((x (_ A /\ -. x = (/)) /\ y ~~ x) <-> ((x (_ A /\ -. x = (/)) /\ v ~~ x)))
15	14	imbi1d 465	. . . . . . . . . . . . 13 |- (y = v -> ((((x (_ A /\ -. x = (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x (_ A /\ -. x = (/)) /\ v ~~ x) -> |^|x e. A)))
16	15	bialdv 935	. . . . . . . . . . . 12 |- (y = v -> (A.x(((x (_ A /\ -. x = (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x (_ A /\ -. x = (/)) /\ v ~~ x) -> |^|x e. A)))
17		breq1 2065	. . . . . . . . . . . . . . 15 |- (y = suc v -> (y ~~ x <-> suc v ~~ x))
18	17	anbi2d 468	. . . . . . . . . . . . . 14 |- (y = suc v -> (((x (_ A /\ -. x = (/)) /\ y ~~ x) <-> ((x (_ A /\ -. x = (/)) /\ suc v ~~ x)))
19	18	imbi1d 465	. . . . . . . . . . . . 13 |- (y = suc v -> ((((x (_ A /\ -. x = (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x (_ A /\ -. x = (/)) /\ suc v ~~ x) -> |^|x e. A)))
20	19	bialdv 935	. . . . . . . . . . . 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)))
21		visset 1350	. . . . . . . . . . . . . . . . . . . 20 |- x e. V
22	21	ensym 3317	. . . . . . . . . . . . . . . . . . 19 |- ((/) ~~ x -> x ~~ (/))
23		en0 3328	. . . . . . . . . . . . . . . . . . 19 |- (x ~~ (/) <-> x = (/))
24	22, 23	sylib 173	. . . . . . . . . . . . . . . . . 18 |- ((/) ~~ x -> x = (/))
25	24	anim1i 269	. . . . . . . . . . . . . . . . 17 |- (((/) ~~ x /\ -. x = (/)) -> (x = (/) /\ -. x = (/)))
26	25	ancoms 334	. . . . . . . . . . . . . . . 16 |- ((-. x = (/) /\ (/) ~~ x) -> (x = (/) /\ -. x = (/)))
27	26	adantll 309	. . . . . . . . . . . . . . 15 |- (((x (_ A /\ -. x = (/)) /\ (/) ~~ x) -> (x = (/) /\ -. x = (/)))
28		pm3.24 496	. . . . . . . . . . . . . . . 16 |- -. (x = (/) /\ -. x = (/))
29	28	pm2.21i 73	. . . . . . . . . . . . . . 15 |- ((x = (/) /\ -. x = (/)) -> |^|x e. A)
30	27, 29	syl 12	. . . . . . . . . . . . . 14 |- (((x (_ A /\ -. x = (/)) /\ (/) ~~ x) -> |^|x e. A)
31	30	ax-gen 677	. . . . . . . . . . . . 13 |- A.x(((x (_ A /\ -. x = (/)) /\ (/) ~~ x) -> |^|x e. A)
32	31	a1i 7	. . . . . . . . . . . 12 |- (A.z e. A A.w e. A (z i^i w) e. A -> A.x(((x (_ A /\ -. x = (/)) /\ (/) ~~ x) -> |^|x e. A))
33		ax-17 925	. . . . . . . . . . . . . 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)
34		hba1 698	. . . . . . . . . . . . . 14 |- (A.x(((x (_ A /\ -. x = (/)) /\ v ~~ x) -> |^|x e. A) -> A.xA.x(((x (_ A /\ -. x = (/)) /\ v ~~ x) -> |^|x e. A))
35		ssel 1502	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x (_ A -> ((f` v) e. x -> (f` v) e. A))
36		df-f1o 2437	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-1-1-onto->x <-> (f:suc v-1-1->x /\ f:suc v-onto->x))
37	36	pm3.27bd 263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-1-1-onto->x -> f:suc v-onto->x)
38		fof 2788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-onto->x -> f:suc v-->x)
39		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- v e. V
40	39	sucid 2304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- v e. suc v
41		ffvrn 2890	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f:suc v-->x /\ v e. suc v) -> (f` v) e. x)
42	40, 41	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-->x -> (f` v) e. x)
43	37, 38, 42	3syl 21	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc v-1-1-onto->x -> (f` v) e. x)
44	35, 43	syl5 22	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x (_ A -> (f:suc v-1-1-onto->x -> (f` v) e. A))
45	44	imp 277	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x (_ A /\ f:suc v-1-1-onto->x) -> (f` v) e. A)
46	45	adantr 306	. . . . . . . . . . . . . . . . . . . . . 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)
47		imassrn 2611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f"v) (_ ran f
48		f1o2 2804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (f:suc v-1-1-onto->x <-> (f Fn suc v /\ Fun `'f /\ ran f = x))
49		3simp3 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f Fn suc v /\ Fun `'f /\ ran f = x) -> ran f = x)
50	48, 49	sylbi 174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1-onto->x -> ran f = x)
51	50	sseq2d 1528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:suc v-1-1-onto->x -> ((f"v) (_ ran f <-> (f"v) (_ x))
52	47, 51	mpbii 168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc v-1-1-onto->x -> (f"v) (_ x)
53		sstr2 1510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((f"v) (_ x -> (x (_ A -> (f"v) (_ A))
54	52, 53	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f:suc v-1-1-onto->x -> (x (_ A -> (f"v) (_ A))
55	54	anim1d 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:suc v-1-1-onto->x -> ((x (_ A /\ -. (f"v) = (/)) -> ((f"v) (_ A /\ -. (f"v) = (/))))
56		f1of1 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc v-1-1-onto->x -> f:suc v-1-1->x)
57		sssucid 2300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- v (_ suc v
58		f1ores 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f:suc v-1-1->x /\ v (_ suc v) -> (f |` v):v-1-1-onto->(f"v))
59	57, 58	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc v-1-1->x -> (f |` v):v-1-1-onto->(f"v))
60	39	f1oen 3301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((f |` v):v-1-1-onto->(f"v) -> v ~~ (f"v))
61	56, 59, 60	3syl 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f:suc v-1-1-onto->x -> v ~~ (f"v))
62	61	a1d 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:suc v-1-1-onto->x -> ((x (_ A /\ -. (f"v) = (/)) -> v ~~ (f"v)))
63	55, 62	jcad 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:suc v-1-1-onto->x -> ((x (_ A /\ -. (f"v) = (/)) -> (((f"v) (_ A /\ -. (f"v) = (/)) /\ v ~~ (f"v))))
64		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- f e. V
65		imaexg 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f e. V -> (f"v) e. V)
66	64, 65	ax-mp 6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f"v) e. V
67		sseq1 1521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x = (f"v) -> (x (_ A <-> (f"v) (_ A))
68		cleq1 1107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"v) -> (x = (/) <-> (f"v) = (/)))
69	68	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x = (f"v) -> (-. x = (/) <-> -. (f"v) = (/)))
70	67, 69	anbi12d 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (x = (f"v) -> ((x (_ A /\ -. x = (/)) <-> ((f"v) (_ A /\ -. (f"v) = (/))))
71		breq2 2066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (x = (f"v) -> (v ~~ x <-> v ~~ (f"v)))
72	70, 71	anbi12d 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31