Theorem fiint 5872

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

Distinct variable group:   x,y,A

Proof of Theorem fiint

Step	Hyp	Ref	Expression
1		isfi 5602	. . . . . . 7 |- (x e. Fin <-> E.y e. om x ~~ y)
2		visset 2541	. . . . . . . . . 10 |- y e. _V
3	2	ensym 5632	. . . . . . . . 9 |- (x ~~ y -> y ~~ x)
4		breq1 3510	. . . . . . . . . . . . . . . 16 |- (y = (/) -> (y ~~ x <-> (/) ~~ x))
5	4	anbi2d 751	. . . . . . . . . . . . . . 15 |- (y = (/) -> (((x C_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x C_ A /\ x =/= (/)) /\ (/) ~~ x)))
6	5	imbi1d 748	. . . . . . . . . . . . . 14 |- (y = (/) -> ((((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x C_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)))
7	6	albidv 1925	. . . . . . . . . . . . 13 |- (y = (/) -> (A.x(((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x C_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)))
8		breq1 3510	. . . . . . . . . . . . . . . 16 |- (y = v -> (y ~~ x <-> v ~~ x))
9	8	anbi2d 751	. . . . . . . . . . . . . . 15 |- (y = v -> (((x C_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x C_ A /\ x =/= (/)) /\ v ~~ x)))
10	9	imbi1d 748	. . . . . . . . . . . . . 14 |- (y = v -> ((((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)))
11	10	albidv 1925	. . . . . . . . . . . . 13 |- (y = v -> (A.x(((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)))
12		breq1 3510	. . . . . . . . . . . . . . . 16 |- (y = suc v -> (y ~~ x <-> suc v ~~ x))
13	12	anbi2d 751	. . . . . . . . . . . . . . 15 |- (y = suc v -> (((x C_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x C_ A /\ x =/= (/)) /\ suc v ~~ x)))
14	13	imbi1d 748	. . . . . . . . . . . . . 14 |- (y = suc v -> ((((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x C_ A /\ x =/= (/)) /\ suc v ~~ x) -> |^|x e. A)))
15	14	albidv 1925	. . . . . . . . . . . . 13 |- (y = suc v -> (A.x(((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x C_ A /\ x =/= (/)) /\ suc v ~~ x) -> |^|x e. A)))
16		visset 2541	. . . . . . . . . . . . . . . . . . . . 21 |- x e. _V
17	16	ensym 5632	. . . . . . . . . . . . . . . . . . . 20 |- ((/) ~~ x -> x ~~ (/))
18		en0 5643	. . . . . . . . . . . . . . . . . . . 20 |- (x ~~ (/) <-> x = (/))
19	17, 18	sylib 242	. . . . . . . . . . . . . . . . . . 19 |- ((/) ~~ x -> x = (/))
20	19	anim1i 538	. . . . . . . . . . . . . . . . . 18 |- (((/) ~~ x /\ x =/= (/)) -> (x = (/) /\ x =/= (/)))
21	20	ancoms 416	. . . . . . . . . . . . . . . . 17 |- ((x =/= (/) /\ (/) ~~ x) -> (x = (/) /\ x =/= (/)))
22	21	adantll 775	. . . . . . . . . . . . . . . 16 |- (((x C_ A /\ x =/= (/)) /\ (/) ~~ x) -> (x = (/) /\ x =/= (/)))
23		df-ne 2268	. . . . . . . . . . . . . . . . 17 |- (x =/= (/) <-> -. x = (/))
24		pm3.24 972	. . . . . . . . . . . . . . . . . 18 |- -. (x = (/) /\ -. x = (/))
25	24	pm2.21i 126	. . . . . . . . . . . . . . . . 17 |- ((x = (/) /\ -. x = (/)) -> |^|x e. A)
26	23, 25	sylan2b 601	. . . . . . . . . . . . . . . 16 |- ((x = (/) /\ x =/= (/)) -> |^|x e. A)
27	22, 26	syl 13	. . . . . . . . . . . . . . 15 |- (((x C_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)
28	27	ax-gen 1593	. . . . . . . . . . . . . 14 |- A.x(((x C_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)
29	28	a1i 8	. . . . . . . . . . . . 13 |- (A.z e. A A.w e. A (z i^i w) e. A -> A.x(((x C_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A))
30		ax-17 1605	. . . . . . . . . . . . . . 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)
31		hba1 1639	. . . . . . . . . . . . . . 15 |- (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> A.xA.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A))
32	16	bren 5597	. . . . . . . . . . . . . . . . . . 19 |- (suc v ~~ x <-> E.f f:suc v-1-1-onto->x)
33		f1ofo 4729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-1-1-onto->x -> f:suc v-onto->x)
34		fof 4705	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-onto->x -> f:suc v-->x)
35		visset 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- v e. _V
36	35	sucid 3889	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- v e. suc v
37		ffvelrn 4877	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f:suc v-->x /\ v e. suc v) -> (f` v) e. x)
38	36, 37	mpan2 679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-->x -> (f` v) e. x)
39	33, 34, 38	3syl 41	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-1-1-onto->x -> (f` v) e. x)
40		ssel 2846	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x C_ A -> ((f` v) e. x -> (f` v) e. A))
41	39, 40	syl5 35	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x C_ A -> (f:suc v-1-1-onto->x -> (f` v) e. A))
42	41	imp 393	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x C_ A /\ f:suc v-1-1-onto->x) -> (f` v) e. A)
43	42	adantr 447	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((x C_ A /\ f:suc v-1-1-onto->x) /\ (A.x(((x C_ 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)
44		df-ne 2268	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f"v) =/= (/) <-> -. (f"v) = (/))
45		imassrn 4396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f"v) C_ ran f
46		dff1o2 4727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (f:suc v-1-1-onto->x <-> (f Fn suc v /\ Fun `'f /\ ran f = x))
47	46	simp3bi 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (f:suc v-1-1-onto->x -> ran f = x)
48	47	sseq2d 2872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f:suc v-1-1-onto->x -> ((f"v) C_ ran f <-> (f"v) C_ x))
49	45, 48	mpbii 319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (f:suc v-1-1-onto->x -> (f"v) C_ x)
50		sstr2 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f"v) C_ x -> (x C_ A -> (f"v) C_ A))
51	49, 50	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1-onto->x -> (x C_ A -> (f"v) C_ A))
52	51	anim1d 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:suc v-1-1-onto->x -> ((x C_ A /\ (f"v) =/= (/)) -> ((f"v) C_ A /\ (f"v) =/= (/))))
53		f1of1 4722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1-onto->x -> f:suc v-1-1->x)
54		sssucid 3887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- v C_ suc v
55		f1ores 4737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f:suc v-1-1->x /\ v C_ suc v) -> (f |` v):v-1-1-onto->(f"v))
56	54, 55	mpan2 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1->x -> (f |` v):v-1-1-onto->(f"v))
57	35	f1oen 5618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f |` v):v-1-1-onto->(f"v) -> v ~~ (f"v))
58	53, 56, 57	3syl 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:suc v-1-1-onto->x -> v ~~ (f"v))
59	52, 58	jctird 508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc v-1-1-onto->x -> ((x C_ A /\ (f"v) =/= (/)) -> (((f"v) C_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v))))
60		visset 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- f e. _V
61		imaexg 4397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f e. _V -> (f"v) e. _V)
62	60, 61	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f"v) e. _V
63		sseq1 2865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = (f"v) -> (x C_ A <-> (f"v) C_ A))
64		neeq1 2273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = (f"v) -> (x =/= (/) <-> (f"v) =/= (/)))
65	63, 64	anbi12d 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> ((x C_ A /\ x =/= (/)) <-> ((f"v) C_ A /\ (f"v) =/= (/))))
66		breq2 3511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> (v ~~ x <-> v ~~ (f"v)))
67	65, 66	anbi12d 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"v) -> (((x C_ A /\ x =/= (/)) /\ v ~~ x) <-> (((f"v) C_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v))))
68		inteq 3403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> |^|x = |^|(f"v))
69	68	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"v) -> (|^|x e. A <-> |^|(f"v) e. A))
70	67, 69	imbi12d 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x = (f"v) -> ((((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) <-> ((((f"v) C_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v)) -> |^|(f"v) e. A)))
71	62, 70	cla4v 2610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> ((((f"v) C_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v)) -> |^|(f"v) e. A))
72	59, 71	sylan9 655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((f:suc v-1-1-onto->x /\ A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)) -> ((x C_ A /\ (f"v) =/= (/)) -> |^|(f"v) e. A))
73		ineq1 3002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (z = |^|(f"v) -> (z i^i w) = (|^|(f"v) i^i w))
74	73	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (z = |^|(f"v) -> ((z i^i w) e. A <-> (|^|(f"v) i^i w) e. A))
75		ineq2 3003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (w = (f` v) -> (|^|(f"v) i^i w) = (|^|(f"v) i^i (f` v)))
76	75	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (w = (f` v) -> ((|^|(f"v) i^i w) e. A <-> (|^|(f"v) i^i (f` v)) e. A))
77	74, 76	rcla42v 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((|^|(f"v) e. A /\ (f` v) e. A) -> (A.z e. A A.w e. A (z i^i w) e. A -> (|^|(f"v) i^i (f` v)) e. A))
78	77	ex 398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (|^|(f"v) e. A -> ((f` v) e. A -> (A.z e. A A.w e. A (z i^i w) e. A -> (|^|(f"v) i^i (f` v)) e. A)))
79	72, 78	syl6 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f:suc v-1-1-onto->x /\ A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)) -> ((x C_ A /\ (f"v) =/= (/)) -> ((f` v) e. A -> (A.z e. A A.w e. A (z i^i w) e. A -> (|^|(f"v) i^i (f` v)) e. A))))
80	79	com4r 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A.z e. A A.w e. A (z i^i w) e. A -> ((f:suc v-1-1-onto->x /\ A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)) -> ((x C_ A /\ (f"v) =/= (/)) -> ((f` v) e. A -> (|^|(f"v) i^i (f` v)) e. A))))
81	80	exp4a 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A.z e. A A.w e. A (z i^i w) e. A -> ((f:suc v-1-1-onto->x /\ A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)) -> (x C_ A -> ((f"v) =/= (/) -> ((f` v) e. A -> (|^|(f"v) i^i (f` v)) e. A)))))
82	81	exp3a 400	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A.z e. A A.w e. A (z i^i w) e. A -> (f:suc v-1-1-onto->x -> (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> (x C_ A -> ((f"v) =/= (/) -> ((f` v) e. A -> (|^|(f"v) i^i (f` v)) e. A))))))
83	82	com14 80	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x C_ A -> (f:suc v-1-1-onto->x -> (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> (A.z e. A A.w e. A (z i^i w) e. A -> ((f"v) =/= (/) -> ((f` v) e. A -> (|^|(f"v) i^i (f` v)) e. A))))))
84	83	imp43 571	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((x C_ A /\ f:suc v-1-1-onto->x) /\ (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) /\ A.z e. A A.w e. A (z i^i w) e. A)) -> ((f"v) =/= (/) -> ((f` v) e. A -> (|^|(f"v) i^i (f` v)) e. A)))
85	44, 84	syl5bir 251	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((x C_ A /\ f:suc v-1-1-onto->x) /\ (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) /\ A.z e. A A.w e. A (z i^i w) e. A)) -> (-. (f"v) = (/) -> ((f` v) e. A -> (|^|(f"v) i^i (f` v)) e. A)))
86		inteq 3403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f"v) = (/) -> |^|(f"v) = |^|(/))
87		int0 3414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- |^|(/) = _V
88	86, 87	syl6eq 2193	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f"v) = (/) -> |^|(f"v) = _V)
89	88	ineq1d 3008	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f"v) = (/) -> (|^|(f"v) i^i (f` v)) = (_V i^i (f` v)))
90		ssv 2864	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f` v) C_ _V
91		sseqin2 3025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f` v) C_ _V <-> (_V i^i (f` v)) = (f` v))
92	90, 91	mpbi 272	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (_V i^i (f` v)) = (f` v)
93	89, 92	syl6eq 2193	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f"v) = (/) -> (|^|(f"v) i^i (f` v)) = (f` v))
94	93	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f"v) = (/) -> ((|^|(f"v) i^i (f` v)) e. A <-> (f` v) e. A))
95	94	biimprd 232	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f"v) = (/) -> ((f` v) e. A -> (|^|(f"v) i^i (f` v)) e. A))
96	85, 95	pm2.61d2 196	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((x C_ A /\ f:suc v-1-1-onto->x) /\ (A.x(((x C_ 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 -> (|^|(f"v) i^i (f` v)) e. A))
97	43, 96	mpd 11	. . . . . . . . . . . . . . . . . . . . . 22 |- (((x C_ A /\ f:suc v-1-1-onto->x) /\ (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) /\ A.z e. A A.w e. A (z i^i w) e. A)) -> (|^|(f"v) i^i (f` v)) e. A)
98		fvex 4778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f` v) e. _V
99	98	intunsn 3435	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- |^|((f"v) u. {(f` v)}) = (|^|(f"v) i^i (f` v))
100		f1ofn 4724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:suc v-1-1-onto->x -> f Fn suc v)
101		fnsnfv 4812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f Fn suc v /\ v e. suc v) -> {(f` v)} = (f"{v}))
102	100, 36, 101	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:suc v-1-1-onto->x -> {(f` v)} = (f"{v}))
103	102	uneq2d 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:suc v-1-1-onto->x -> ((f"v) u. {(f` v)}) = ((f"v) u. (f"{v})))
104		df-suc 3817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- suc v = (v u. {v})
105	104	imaeq2i 4382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f"suc v) = (f"(v u. {v}))
106		imaundi 4437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f"(v u. {v})) = ((f"v) u. (f"{v}))
107	105, 106	eqtr2i 2162	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f"v) u. (f"{v})) = (f"suc v)
108	103, 107	syl6eq 2193	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-1-1-onto->x -> ((f"v) u. {(f` v)}) = (f"suc v))
109		foima 4710	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:suc v-onto->x -> (f"suc v) = x)
110	33, 109	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-1-1-onto->x -> (f"suc v) = x)
111	108, 110	eqtrd 2173	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-1-1-onto->x -> ((f"v) u. {(f` v)}) = x)
112	111	inteqd 3405	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc v-1-1-onto->x -> |^|((f"v) u. {(f` v)}) = |^|x)
113	99, 112	syl5eqr 2189	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:suc v-1-1-onto->x -> (|^|(f"v) i^i (f` v)) = |^|x)
114	113	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f:suc v-1-1-onto->x -> ((|^|(f"v) i^i (f` v)) e. A <-> |^|x e. A))
115	114	ad2antlr 802	. . . . . . . . . . . . . . . . . . . . . 22 |- (((x C_ A /\ f:suc v-1-1-onto->x) /\ (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) /\ A.z e. A A.w e. A (z i^i w) e. A)) -> ((|^|(f"v) i^i (f` v)) e. A <-> |^|x e. A))
116	97, 115	mpbid 317	. . . . . . . . . . . . . . . . . . . . 21 |- (((x C_ A /\ f:suc v-1-1-onto->x) /\ (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) /\ A.z e. A A.w e. A (z i^i w) e. A)) -> |^|x e. A)
117	116	exp43 586	. . . . . . . . . . . . . . . . . . . 20 |- (x C_ A -> (f:suc v-1-1-onto->x -> (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> (A.z e. A A.w e. A (z i^i w) e. A -> |^|x e. A))))
118	117	19.23adv 1860	. . . . . . . . . . . . . . . . . . 19 |- (x C_ A -> (E.f f:suc v-1-1-onto->x -> (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> (A.z e. A A.w e. A (z i^i w) e. A -> |^|x e. A))))
119	32, 118	syl5bi 249	. . . . . . . . . . . . . . . . . 18 |- (x C_ A -> (suc v ~~ x -> (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> (A.z e. A A.w e. A (z i^i w) e. A -> |^|x e. A))))
120	119	imp 393	. . . . . . . . . . . . . . . . 17 |- ((x C_ A /\ suc v ~~ x) -> (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> (A.z e. A A.w e. A (z i^i w) e. A -> |^|x e. A)))
121	120	adantlr 777	. . . . . . . . . . . . . . . 16 |- (((x C_ A /\ x =/= (/)) /\ suc v ~~ x) -> (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> (A.z e. A A.w e. A (z i^i w) e. A -> |^|x e. A)))
122	121	com13 67	. . . . . . . . . . . . . . 15 |- (A.z e. A A.w e. A (z i^i w) e. A -> (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> (((x C_ A /\ x =/= (/)) /\ suc v ~~ x) -> |^|x e. A)))
123	30, 31, 122	19.21ad 1695	. . . . . . . . . . . . . 14 |- (A.z e. A A.w e. A (z i^i w) e. A -> (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> A.x(((x C_ A /\ x =/= (/)) /\ suc v ~~ x) -> |^|x e. A)))
124	123	a1i 8	. . . . . . . . . . . . 13 |- (v e. om -> (A.z e. A A.w e. A (z i^i w) e. A -> (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> A.x(((x C_ A /\ x =/= (/)) /\ suc v ~~ x) -> |^|x e. A))))
125	7, 11, 15, 29, 124	finds2 4114	. . . . . . . . . . . 12 |- (y e. om -> (A.z e. A A.w e. A (z i^i w) e. A -> A.x(((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A)))
126		ax-4 1608	. . . . . . . . . . . 12 |- (A.x(((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) -> (((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A))
127	125, 126	syl6 42	. . . . . . . . . . 11 |- (y e. om -> (A.z e. A A.w e. A (z i^i w) e. A -> (((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A)))
128	127	exp4a 579	. . . . . . . . . 10 |- (y e. om -> (A.z e. A A.w e. A (z i^i w) e. A -> ((x C_ A /\ x =/= (/)) -> (y ~~ x -> |^|x e. A))))
129	128	com24 79	. . . . . . . . 9 |- (y e. om -> (y ~~ x -> ((x C_ A /\ x =/= (/)) -> (A.z e. A A.w e. A (z i^i w) e. A -> |^|x e. A))))
130	3, 129	syl5 35	. . . . . . . 8 |- (y e. om -> (x ~~ y -> ((x C_ A /\ x =/= (/)) -> (A.z e. A A.w e. A (z i^i w) e. A -> |^|x e. A))))
131	130	r19.23aiv 2459	. . . . . . 7 |- (E.y e. om x ~~ y -> ((x C_ A /\ x =/= (/)) -> (A.z e. A A.w e. A (z i^i w) e. A -> |^|x e. A)))
132	1, 131	sylbi 225	. . . . . 6 |- (x e. Fin -> ((x C_ A /\ x =/= (/)) -> (A.z e. A A.w e. A (z i^i w) e. A -> |^|x e. A)))
133	132	com13 67	. . . . 5 |- (A.z e. A A.w e. A (z i^i w) e. A -> ((x C_ A /\ x =/= (/)) -> (x e. Fin -> |^|x e. A)))
134	133	imp3a 395	. . . 4 |- (A.z e. A A.w e. A (z i^i w) e. A -> (((x C_ A /\ x =/= (/)) /\ x e. Fin) -> |^|x e. A))
135	134	19.21aiv 1933	. . 3 |- (A.z e. A A.w e. A (z i^i w) e. A -> A.x(((x C_ A /\ x =/= (/)) /\ x e. Fin) -> |^|x e. A))
136		zfpair2 3688	. . . . . 6 |- {z, w} e. _V
137		sseq1 2865	. . . . . . . . 9 |- (x = {z, w} -> (x C_ A <-> {z, w} C_ A))
138		neeq1 2273	. . . . . . . . 9 |- (x = {z, w} -> (x =/= (/) <-> {z, w} =/= (/)))
139	137, 138	anbi12d 763	. . . . . . . 8 |- (x = {z, w} -> ((x C_ A /\ x =/= (/)) <-> ({z, w} C_ A /\ {z, w} =/= (/))))
140		eleq1 2204	. . . . . . . 8 |- (x = {z, w} -> (x e. Fin <-> {z, w} e. Fin))
141	139, 140	anbi12d 763	. . . . . . 7 |- (x = {z, w} -> (((x C_ A /\ x =/= (/)) /\ x e. Fin) <-> (({z, w} C_ A /\ {z, w} =/= (/)) /\ {z, w} e. Fin)))
142		inteq 3403	. . . . . . . 8 |- (x = {z, w} -> |^|x = |^|{z, w})
143	142	eleq1d 2210	. . . . . . 7 |- (x = {z, w} -> (|^|x e. A <-> |^|{z, w} e. A))
144	141, 143	imbi12d 761	. . . . . 6 |- (x = {z, w} -> ((((x C_ A /\ x =/= (/)) /\ x e. Fin) -> |^|x e. A) <-> ((({z, w} C_ A /\ {z, w} =/= (/)) /\ {z, w} e. Fin) -> |^|{z, w} e. A)))
145	136, 144	cla4v 2610	. . . . 5 |- (A.x(((x C_ A /\ x =/= (/)) /\ x e. Fin) -> |^|x e. A) -> ((({z, w} C_ A /\ {z, w} =/= (/)) /\ {z, w} e. Fin) -> |^|{z, w} e. A))
146		visset 2541	. . . . . . 7 |- z e. _V
147		visset 2541	. . . . . . 7 |- w e. _V
148	146, 147	prss 3329	. . . . . 6 |- ((z e. A /\ w e. A) <-> {z, w} C_ A)
149	146	prnz 3314	. . . . . . 7 |- {z, w} =/= (/)
150	149	biantru 953	. . . . . 6 |- ({z, w} C_ A <-> ({z, w} C_ A /\ {z, w} =/= (/)))
151		prfi 5869	. . . . . . 7 |- {z, w} e. Fin
152	151	biantru 953	. . . . . 6 |- (({z, w} C_ A /\ {z, w} =/= (/)) <-> (({z, w} C_ A /\ {z, w} =/= (/)) /\ {z, w} e. Fin))
153	148, 150, 152	3bitrri 290	. . . . 5 |- ((({z, w} C_ A /\ {z, w} =/= (/)) /\ {z, w} e. Fin) <-> (z e. A /\ w e. A))
154	146, 147	intpr 3431	. . . . . 6 |- |^|{z, w} = (z i^i w)
155	154	eleq1i 2207	. . . . 5 |- (|^|{z, w} e. A <-> (z i^i w) e. A)
156	145, 153, 155	3imtr3g 331	. . . 4 |- (A.x(((x C_ A /\ x =/= (/)) /\ x e. Fin) -> |^|x e. A) -> ((z e. A /\ w e. A) -> (z i^i w) e. A))
157	156	r19.21aivv 2433	. . 3 |- (A.x(((x C_ A /\ x =/= (/)) /\ x e. Fin) -> |^|x e. A) -> A.z e. A A.w e. A (z i^i w) e. A)
158	135, 157	impbii 223	. 2 |- (A.z e. A A.w e. A (z i^i w) e. A <-> A.x(((x C_ A /\ x =/= (/)) /\ x e. Fin) -> |^|x e. A))
159		ineq1 3002	. . . 4 |- (x = z -> (x i^i y) = (z i^i y))
160	159	eleq1d 2210	. . 3 |- (x = z -> ((x i^i y) e. A <-> (z i^i y) e. A))
161		ineq2 3003	. . . 4 |- (y = w -> (z i^i y) = (z i^i w))
162	161	eleq1d 2210	. . 3 |- (y = w -> ((z i^i y) e. A <-> (z i^i w) e. A))
163	160, 162	cbvral2v 2529	. 2 |- (A.x e. A A.y e. A (x i^i y) e. A <-> A.z e. A A.w e. A (z i^i w) e. A)
164		df-3an 1104	. . . 4 |- ((x C_ A /\ x =/= (/) /\ x e. Fin) <-> ((x C_ A /\ x =/= (/)) /\ x e. Fin))
165	164	imbi1i 299	. . 3 |- (((x C_ A /\ x =/= (/) /\ x e. Fin) -> |^|x e. A) <-> (((x C_ A /\ x =/= (/)) /\ x e. Fin) -> |^|x e. A))
166	165	albii 1635	. 2 |- (A.x((x C_ A /\ x =/= (/) /\ x e. Fin) -> |^|x e. A) <-> A.x(((x C_ A /\ x =/= (/)) /\ x e. Fin) -> |^|x e. A))
167	158, 163, 166	3bitr4i 295	1 |- (A.x e. A A.y e. A (x i^i y) e. A <-> A.x((x C_ A /\ x =/= (/) /\ x e. Fin) -> |^|x e. A))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102  A.wal 1584   = wceq 1586   e. wcel 1588  E.wex 1615   =/= wne 2266  A.wral 2355  E.wrex 2356  _Vcvv 2538   u. cun 2825   i^i cin 2826   C_ wss 2827  (/)c0 3082  {csn 3238  {cpr 3239  |^|cint 3400   class class class wbr 3507  suc csuc 3813  omcom 4085  `'ccnv 4118  ran crn 4120   |` cres 4121  "cima 4122  Fun wfun 4125   Fn wfn 4126  -->wf 4127  -1-1->wf1 4128  -onto->wfo 4129  -1-1-onto->wf1o 4130  ` cfv 4131   ~~ cen 5584  Fincfn 5587

This theorem is referenced by:  abfii1 5873  abfii4 5876  istop2g 9701  istps4OLD 9715  istps4 9720  inficlALT 11047  fipfil2 11110  filint2 15689  inficlALTOLD 16196

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-rdg 5304  df-1o 5344  df-oadd 5346  df-er 5479  df-en 5588  df-fin 5591

Copyright terms: Public domain