Theorem fiint 4644

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 =/= (/) /\ x e. Fin) -> |^|x e. A))

Distinct variable group:   x,y,A

Proof of Theorem fiint

Step	Hyp	Ref	Expression
1		isfi 4469	. . . . . . 7 |- (x e. Fin <-> E.y e. om x ~~ y)
2		breq1 2672	. . . . . . . . . . . . . . . 16 |- (y = (/) -> (y ~~ x <-> (/) ~~ x))
3	2	anbi2d 618	. . . . . . . . . . . . . . 15 |- (y = (/) -> (((x (_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x (_ A /\ x =/= (/)) /\ (/) ~~ x)))
4	3	imbi1d 615	. . . . . . . . . . . . . 14 |- (y = (/) -> ((((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)))
5	4	albidv 1311	. . . . . . . . . . . . 13 |- (y = (/) -> (A.x(((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)))
6		breq1 2672	. . . . . . . . . . . . . . . 16 |- (y = v -> (y ~~ x <-> v ~~ x))
7	6	anbi2d 618	. . . . . . . . . . . . . . 15 |- (y = v -> (((x (_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x (_ A /\ x =/= (/)) /\ v ~~ x)))
8	7	imbi1d 615	. . . . . . . . . . . . . 14 |- (y = v -> ((((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)))
9	8	albidv 1311	. . . . . . . . . . . . 13 |- (y = v -> (A.x(((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)))
10		breq1 2672	. . . . . . . . . . . . . . . 16 |- (y = suc v -> (y ~~ x <-> suc v ~~ x))
11	10	anbi2d 618	. . . . . . . . . . . . . . 15 |- (y = suc v -> (((x (_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x (_ A /\ x =/= (/)) /\ suc v ~~ x)))
12	11	imbi1d 615	. . . . . . . . . . . . . 14 |- (y = suc v -> ((((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x (_ A /\ x =/= (/)) /\ suc v ~~ x) -> |^|x e. A)))
13	12	albidv 1311	. . . . . . . . . . . . 13 |- (y = suc v -> (A.x(((x (_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x (_ A /\ x =/= (/)) /\ suc v ~~ x) -> |^|x e. A)))
14		visset 1851	. . . . . . . . . . . . . . . . . . . . 21 |- x e. V
15	14	ensym 4499	. . . . . . . . . . . . . . . . . . . 20 |- ((/) ~~ x -> x ~~ (/))
16		en0 4510	. . . . . . . . . . . . . . . . . . . 20 |- (x ~~ (/) <-> x = (/))
17	15, 16	sylib 196	. . . . . . . . . . . . . . . . . . 19 |- ((/) ~~ x -> x = (/))
18	17	anim1i 332	. . . . . . . . . . . . . . . . . 18 |- (((/) ~~ x /\ x =/= (/)) -> (x = (/) /\ x =/= (/)))
19	18	ancoms 438	. . . . . . . . . . . . . . . . 17 |- ((x =/= (/) /\ (/) ~~ x) -> (x = (/) /\ x =/= (/)))
20	19	adantll 392	. . . . . . . . . . . . . . . 16 |- (((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> (x = (/) /\ x =/= (/)))
21		pm3.24 660	. . . . . . . . . . . . . . . . . 18 |- -. (x = (/) /\ -. x = (/))
22	21	pm2.21i 77	. . . . . . . . . . . . . . . . 17 |- ((x = (/) /\ -. x = (/)) -> |^|x e. A)
23		df-ne 1624	. . . . . . . . . . . . . . . . 17 |- (x =/= (/) <-> -. x = (/))
24	22, 23	sylan2b 454	. . . . . . . . . . . . . . . 16 |- ((x = (/) /\ x =/= (/)) -> |^|x e. A)
25	20, 24	syl 10	. . . . . . . . . . . . . . 15 |- (((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)
26	25	ax-gen 995	. . . . . . . . . . . . . 14 |- A.x(((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)
27	26	a1i 8	. . . . . . . . . . . . 13 |- (A.z e. A A.w e. A (z i^i w) e. A -> A.x(((x (_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A))
28		ax-17 1003	. . . . . . . . . . . . . . 15 |- (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)
29		hba1 1035	. . . . . . . . . . . . . . 15 |- (A.x(((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> A.xA.x(((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A))
30		ssel 2107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x (_ A -> ((f` v) e. x -> (f` v) e. A))
31		f1ofo 3771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-1-1-onto->x -> f:suc v-onto->x)
32		fof 3747	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-onto->x -> f:suc v-->x)
33		visset 1851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- v e. V
34	33	sucid 3106	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- v e. suc v
35		ffvelrn 3890	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f:suc v-->x /\ v e. suc v) -> (f` v) e. x)
36	34, 35	mpan2 699	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-->x -> (f` v) e. x)
37	31, 32, 36	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-1-1-onto->x -> (f` v) e. x)
38	30, 37	syl5 21	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x (_ A -> (f:suc v-1-1-onto->x -> (f` v) e. A))
39	38	imp 348	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x (_ A /\ f:suc v-1-1-onto->x) -> (f` v) e. A)
40	39	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((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)
41		imassrn 3478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f"v) (_ ran f
42		dff1o2 3769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (f:suc v-1-1-onto->x <-> (f Fn suc v /\ Fun `'f /\ ran f = x))
43		3simp3 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((f Fn suc v /\ Fun `'f /\ ran f = x) -> ran f = x)
44	42, 43	sylbi 197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (f:suc v-1-1-onto->x -> ran f = x)
45	44	sseq2d 2133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f:suc v-1-1-onto->x -> ((f"v) (_ ran f <-> (f"v) (_ x))
46	41, 45	mpbii 191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (f:suc v-1-1-onto->x -> (f"v) (_ x)
47		sstr2 2115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f"v) (_ x -> (x (_ A -> (f"v) (_ A))
48	46, 47	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1-onto->x -> (x (_ A -> (f"v) (_ A))
49	48	anim1d 562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:suc v-1-1-onto->x -> ((x (_ A /\ (f"v) =/= (/)) -> ((f"v) (_ A /\ (f"v) =/= (/))))
50		f1of1 3764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1-onto->x -> f:suc v-1-1->x)
51		sssucid 3102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- v (_ suc v
52		f1ores 3779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f:suc v-1-1->x /\ v (_ suc v) -> (f |` v):v-1-1-onto->(f"v))
53	51, 52	mpan2 699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1->x -> (f |` v):v-1-1-onto->(f"v))
54	33	f1oen 4485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f |` v):v-1-1-onto->(f"v) -> v ~~ (f"v))
55	50, 53, 54	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:suc v-1-1-onto->x -> v ~~ (f"v))
56	49, 55	jctird 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc v-1-1-onto->x -> ((x (_ A /\ (f"v) =/= (/)) -> (((f"v) (_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v))))
57		visset 1851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- f e. V
58		imaexg 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f e. V -> (f"v) e. V)
59	57, 58	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f"v) e. V
60		sseq1 2126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = (f"v) -> (x (_ A <-> (f"v) (_ A))
61		neeq1 1627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = (f"v) -> (x =/= (/) <-> (f"v) =/= (/)))
62	60, 61	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> ((x (_ A /\ x =/= (/)) <-> ((f"v) (_ A /\ (f"v) =/= (/))))
63		breq2 2673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> (v ~~ x <-> v ~~ (f"v)))
64	62, 63	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"v) -> (((x (_ A /\ x =/= (/)) /\ v ~~ x) <-> (((f"v) (_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v))))
65		inteq 2584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> |^|x = |^|(f"v))
66	65	eleq1d 1577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"v) -> (|^|x e. A <-> |^|(f"v) e. A))
67	64, 66	imbi12d 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x = (f"v) -> ((((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) <-> ((((f"v) (_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v)) -> |^|(f"v) e. A)))
68	59, 67	cla4v 1906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (A.x(((x (_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> ((((f"v) (_ A /\ (f"