Theorem fiint 5650

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 5441	. . . . . . 7 |- (x e. Fin <-> E.y e. om x ~~ y)
2		breq1 3341	. . . . . . . . . . . . . . . 16 |- (y = (/) -> (y ~~ x <-> (/) ~~ x))
3	2	anbi2d 678	. . . . . . . . . . . . . . 15 |- (y = (/) -> (((x C_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x C_ A /\ x =/= (/)) /\ (/) ~~ x)))
4	3	imbi1d 675	. . . . . . . . . . . . . 14 |- (y = (/) -> ((((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x C_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)))
5	4	albidv 1656	. . . . . . . . . . . . 13 |- (y = (/) -> (A.x(((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> A.x(((x C_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)))
6		breq1 3341	. . . . . . . . . . . . . . . 16 |- (y = v -> (y ~~ x <-> v ~~ x))
7	6	anbi2d 678	. . . . . . . . . . . . . . 15 |- (y = v -> (((x C_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x C_ A /\ x =/= (/)) /\ v ~~ x)))
8	7	imbi1d 675	. . . . . . . . . . . . . 14 |- (y = v -> ((((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A)))
9	8	albidv 1656	. . . . . . . . . . . . 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)))
10		breq1 3341	. . . . . . . . . . . . . . . 16 |- (y = suc v -> (y ~~ x <-> suc v ~~ x))
11	10	anbi2d 678	. . . . . . . . . . . . . . 15 |- (y = suc v -> (((x C_ A /\ x =/= (/)) /\ y ~~ x) <-> ((x C_ A /\ x =/= (/)) /\ suc v ~~ x)))
12	11	imbi1d 675	. . . . . . . . . . . . . 14 |- (y = suc v -> ((((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) <-> (((x C_ A /\ x =/= (/)) /\ suc v ~~ x) -> |^|x e. A)))
13	12	albidv 1656	. . . . . . . . . . . . 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)))
14		visset 2295	. . . . . . . . . . . . . . . . . . . . 21 |- x e. _V
15	14	ensym 5471	. . . . . . . . . . . . . . . . . . . 20 |- ((/) ~~ x -> x ~~ (/))
16		en0 5482	. . . . . . . . . . . . . . . . . . . 20 |- (x ~~ (/) <-> x = (/))
17	15, 16	sylib 215	. . . . . . . . . . . . . . . . . . 19 |- ((/) ~~ x -> x = (/))
18	17	anim1i 361	. . . . . . . . . . . . . . . . . 18 |- (((/) ~~ x /\ x =/= (/)) -> (x = (/) /\ x =/= (/)))
19	18	ancoms 484	. . . . . . . . . . . . . . . . 17 |- ((x =/= (/) /\ (/) ~~ x) -> (x = (/) /\ x =/= (/)))
20	19	adantll 428	. . . . . . . . . . . . . . . 16 |- (((x C_ A /\ x =/= (/)) /\ (/) ~~ x) -> (x = (/) /\ x =/= (/)))
21		pm3.24 720	. . . . . . . . . . . . . . . . . 18 |- -. (x = (/) /\ -. x = (/))
22	21	pm2.21i 93	. . . . . . . . . . . . . . . . 17 |- ((x = (/) /\ -. x = (/)) -> |^|x e. A)
23		df-ne 2019	. . . . . . . . . . . . . . . . 17 |- (x =/= (/) <-> -. x = (/))
24	22, 23	sylan2b 501	. . . . . . . . . . . . . . . 16 |- ((x = (/) /\ x =/= (/)) -> |^|x e. A)
25	20, 24	syl 12	. . . . . . . . . . . . . . 15 |- (((x C_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A)
26	25	ax-gen 1305	. . . . . . . . . . . . . 14 |- A.x(((x C_ 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 C_ A /\ x =/= (/)) /\ (/) ~~ x) -> |^|x e. A))
28		ax-17 1317	. . . . . . . . . . . . . . 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 1350	. . . . . . . . . . . . . . 15 |- (A.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A) -> A.xA.x(((x C_ A /\ x =/= (/)) /\ v ~~ x) -> |^|x e. A))
30		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x C_ A -> ((f` v) e. x -> (f` v) e. A))
31		f1ofo 4643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-1-1-onto->x -> f:suc v-onto->x)
32		fof 4617	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-onto->x -> f:suc v-->x)
33		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- v e. _V
34	33	sucid 3744	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- v e. suc v
35		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f:suc v-->x /\ v e. suc v) -> (f` v) e. x)
36	34, 35	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-->x -> (f` v) e. x)
37	31, 32, 36	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-1-1-onto->x -> (f` v) e. x)
38	30, 37	syl5 20	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x C_ A -> (f:suc v-1-1-onto->x -> (f` v) e. A))
39	38	imp 377	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x C_ A /\ f:suc v-1-1-onto->x) -> (f` v) e. A)
40	39	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 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)
41		imassrn 4278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f"v) C_ ran f
42		dff1o2 4639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (f:suc v-1-1-onto->x <-> (f Fn suc v /\ Fun `'f /\ ran f = x))
43	42	simp3bi 893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (f:suc v-1-1-onto->x -> ran f = x)
44	43	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f:suc v-1-1-onto->x -> ((f"v) C_ ran f <-> (f"v) C_ x))
45	41, 44	mpbii 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (f:suc v-1-1-onto->x -> (f"v) C_ x)
46		sstr2 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f"v) C_ x -> (x C_ A -> (f"v) C_ A))
47	45, 46	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1-onto->x -> (x C_ A -> (f"v) C_ A))
48	47	anim1d 619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:suc v-1-1-onto->x -> ((x C_ A /\ (f"v) =/= (/)) -> ((f"v) C_ A /\ (f"v) =/= (/))))
49		f1of1 4634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1-onto->x -> f:suc v-1-1->x)
50		sssucid 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- v C_ suc v
51		f1ores 4654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f:suc v-1-1->x /\ v C_ suc v) -> (f |` v):v-1-1-onto->(f"v))
52	50, 51	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:suc v-1-1->x -> (f |` v):v-1-1-onto->(f"v))
53	33	f1oen 5457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f |` v):v-1-1-onto->(f"v) -> v ~~ (f"v))
54	49, 52, 53	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:suc v-1-1-onto->x -> v ~~ (f"v))
55	48, 54	jctird 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc v-1-1-onto->x -> ((x C_ A /\ (f"v) =/= (/)) -> (((f"v) C_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v))))
56		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- f e. _V
57		imaexg 4279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f e. _V -> (f"v) e. _V)
58	56, 57	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f"v) e. _V
59		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = (f"v) -> (x C_ A <-> (f"v) C_ A))
60		neeq1 2024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = (f"v) -> (x =/= (/) <-> (f"v) =/= (/)))
61	59, 60	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> ((x C_ A /\ x =/= (/)) <-> ((f"v) C_ A /\ (f"v) =/= (/))))
62		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> (v ~~ x <-> v ~~ (f"v)))
63	61, 62	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"v) -> (((x C_ A /\ x =/= (/)) /\ v ~~ x) <-> (((f"v) C_ A /\ (f"v) =/= (/)) /\ v ~~ (f"v))))
64		inteq 3217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (f"v) -> |^|x = |^|(f"v))
65	64	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"v) -> (|^|x e. A <-> |^|(f"v) e. A))
66	63, 65	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))
67	58, 66	cla4v 2370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))
68	55, 67	sylan9 517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))
69		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (z = |^|(f"v) -> (z i^i w) = (|^|(f"v) i^i w))
70	69	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (z = |^|(f"v) -> ((z i^i w) e. A <-> (|^|(f"v) i^i w) e. A))
71		ineq2 2790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (w = (f` v) -> (|^|(f"v) i^i w) = (|^|(f"v) i^i (f` v)))
72	71	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (w = (f` v) -> ((|^|(f"v) i^i w) e. A <-> (|^|(f"v) i^i (f` v)) e. A))
73	70, 72	rcla42v 2384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))
74	73	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))
75	68, 74	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
76	75	com4r 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
77	76	exp4a 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))))
78	77	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . . . . 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))))))
79	78	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . 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))))))
80	79	imp43 397	. . . . . . . . . . . . . . . . . . . . . . . . 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)))
81		df-ne 2019	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f"v) =/= (/) <-> -. (f"v) = (/))
82	80, 81	syl5ibr 224	. . . . . . . . . . . . . . . . . . . . . . . 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)))
83		inteq 3217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f"v) = (/) -> |^|(f"v) = |^|(/))
84		int0 3230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- |^|(/) = _V
85	83, 84	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f"v) = (/) -> |^|(f"v) = _V)
86	85	ineq1d 2795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f"v) = (/) -> (|^|(f"v) i^i (f` v)) = (_V i^i (f` v)))
87		ssv 2636	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f` v) C_ _V
88		sseqin2 2811	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f` v) C_ _V <-> (_V i^i (f` v)) = (f` v))
89	87, 88	mpbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (_V i^i (f` v)) = (f` v)
90	86, 89	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f"v) = (/) -> (|^|(f"v) i^i (f` v)) = (f` v))
91	90	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f"v) = (/) -> ((|^|(f"v) i^i (f` v)) e. A <-> (f` v) e. A))
92	91	biimprd 171	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f"v) = (/) -> ((f` v) e. A -> (|^|(f"v) i^i (f` v)) e. A))
93	82, 92	pm2.61d2 143	. . . . . . . . . . . . . . . . . . . . . . 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))
94	40, 93	mpd 29	. . . . . . . . . . . . . . . . . . . . . 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)
95		fnsnfv 4728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f Fn suc v /\ v e. suc v) -> {(f` v)} = (f"{v}))
96		f1ofn 4636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:suc v-1-1-onto->x -> f Fn suc v)
97	95, 96, 34	sylancl 525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:suc v-1-1-onto->x -> {(f` v)} = (f"{v}))
98	97	uneq2d 2755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:suc v-1-1-onto->x -> ((f"v) u. {(f` v)}) = ((f"v) u. (f"{v})))
99		df-suc 3663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- suc v = (v u. {v})
100	99	imaeq2i 4262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f"suc v) = (f"(v u. {v}))
101		imaundi 4328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f"(v u. {v})) = ((f"v) u. (f"{v}))
102	100, 101	eqtr2i 1909	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f"v) u. (f"{v})) = (f"suc v)
103	98, 102	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-1-1-onto->x -> ((f"v) u. {(f` v)}) = (f"suc v))
104		foima 4622	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:suc v-onto->x -> (f"suc v) = x)
105	31, 104	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc v-1-1-onto->x -> (f"suc v) = x)
106	103, 105	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc v-1-1-onto->x -> ((f"v) u. {(f` v)}) = x)
107	106	inteqd 3219	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc v-1-1-onto->x -> |^|((f"v) u. {(f` v)}) = |^|x)
108		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f` v) e. _V
109	108	intunsn 3254	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- |^|((f"v) u. {(f` v)}) = (|^|(f"v) i^i (f` v))
110	107, 109	syl5eqr 1942	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:suc v-1-1-onto->x -> (|^|(f"v) i^i (f` v)) = |^|x)
111	110	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f:suc v-1-1-onto->x -> ((|^|(f"v) i^i (f` v)) e. A <-> |^|x e. A))
112	111	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . 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))
113	94, 112	mpbid 212	. . . . . . . . . . . . . . . . . . . . 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)
114	113	exp43 415	. . . . . . . . . . . . . . . . . . . 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))))
115	114	19.23adv 1584	. . . . . . . . . . . . . . . . . . 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))))
116	14	bren 5436	. . . . . . . . . . . . . . . . . . 19 |- (suc v ~~ x <-> E.f f:suc v-1-1-onto->x)
117	115, 116	syl5ib 223	. . . . . . . . . . . . . . . . . 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))))
118	117	imp 377	. . . . . . . . . . . . . . . . 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)))
119	118	adantlr 429	. . . . . . . . . . . . . . . 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)))
120	119	com13 37	. . . . . . . . . . . . . . 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)))
121	28, 29, 120	19.21ad 1406	. . . . . . . . . . . . . 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)))
122	121	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))))
123	5, 9, 13, 27, 122	finds2 3981	. . . . . . . . . . . 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)))
124		ax-4 1319	. . . . . . . . . . . 12 |- (A.x(((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A) -> (((x C_ A /\ x =/= (/)) /\ y ~~ x) -> |^|x e. A))
125	123, 124	syl6 25	. . . . . . . . . . 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)))
126	125	exp4a 409	. . . . . . . . . 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))))
127	126	com24 41	. . . . . . . . 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))))
128		visset 2295	. . . . . . . . . 10 |- y e. _V
129	128	ensym 5471	. . . . . . . . 9 |- (x ~~ y -> y ~~ x)
130	127, 129	syl5 20	. . . . . . . 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 2211	. . . . . . 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 216	. . . . . 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 37	. . . . 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 388	. . . 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 1664	. . 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 3525	. . . . . 6 |- {z, w} e. _V
137		sseq1 2637	. . . . . . . . 9 |- (x = {z, w} -> (x C_ A <-> {z, w} C_ A))
138		neeq1 2024	. . . . . . . . 9 |- (x = {z, w} -> (x =/= (/) <-> {z, w} =/= (/)))
139	137, 138	anbi12d 690	. . . . . . . 8 |- (x = {z, w} -> ((x C_ A /\ x =/= (/)) <-> ({z, w} C_ A /\ {z, w} =/= (/))))
140		eleq1 1957	. . . . . . . 8 |- (x = {z, w} -> (x e. Fin <-> {z, w} e. Fin))
141	139, 140	anbi12d 690	. . . . . . 7 |- (x = {z, w} -> (((x C_ A /\ x =/= (/)) /\ x e. Fin) <-> (({z, w} C_ A /\ {z, w} =/= (/)) /\ {z, w} e. Fin)))
142		inteq 3217	. . . . . . . 8 |- (x = {z, w} -> |^|x = |^|{z, w})
143	142	eleq1d 1963	. . . . . . 7 |- (x = {z, w} -> (|^|x e. A <-> |^|{z, w} e. A))
144	141, 143	imbi12d 688	. . . . . 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 2370	. . . . 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 2295	. . . . . . 7 |- z e. _V
147		visset 2295	. . . . . . 7 |- w e. _V
148	146, 147	prss 3138	. . . . . 6 |- ((z e. A /\ w e. A) <-> {z, w} C_ A)
149	146	prnz 3120	. . . . . . 7 |- {z, w} =/= (/)
150	149	biantru 793	. . . . . 6 |- ({z, w} C_ A <-> ({z, w} C_ A /\ {z, w} =/= (/)))
151		prfi 5647	. . . . . . 7 |- {z, w} e. Fin
152	151	biantru 793	. . . . . 6 |- (({z, w} C_ A /\ {z, w} =/= (/)) <-> (({z, w} C_ A /\ {z, w} =/= (/)) /\ {z, w} e. Fin))
153	148, 150, 152	3bitrri 195	. . . . 5 |- ((({z, w} C_ A /\ {z, w} =/= (/)) /\ {z, w} e. Fin) <-> (z e. A /\ w e. A))
154	146, 147	intpr 3250	. . . . . 6 |- |^|{z, w} = (z i^i w)
155	154	eleq1i 1960	. . . . 5 |- (|^|{z, w} e. A <-> (z i^i w) e. A)
156	145, 153, 155	3imtr3g 611	. . . 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 2183	. . 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 174	. 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 2789	. . . 4 |- (x = z -> (x i^i y) = (z i^i y))
160	159	eleq1d 1963	. . 3 |- (x = z -> ((x i^i y) e. A <-> (z i^i y) e. A))
161		ineq2 2790	. . . 4 |- (y = w -> (z i^i y) = (z i^i w))
162	161	eleq1d 1963	. . 3 |- (y = w -> ((z i^i y) e. A <-> (z i^i w) e. A))
163	160, 162	cbvral2v 2283	. 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 860	. . . 4 |- ((x C_ A /\ x =/= (/) /\ x e. Fin) <-> ((x C_ A /\ x =/= (/)) /\ x e. Fin))
165	164	imbi1i 203	. . 3 |- (((x C_ A /\ x =/= (/) /\ x e. Fin) -> |^|x e. A) <-> (((x C_ A /\ x =/= (/)) /\ x e. Fin) -> |^|x e. A))
166	165	albii 1346	. 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 200	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 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  {cpr 3045  |^|cint 3214   class class class wbr 3338  suc csuc 3659  omcom 3949  `'ccnv 3985  ran crn 3987   |` cres 3988  "cima 3989  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998   ~~ cen 5423  Fincfn 5426

This theorem is referenced by:  abfii1 5651  abfii4 5654  istop2g 8866  istps4 8878  fipfil2 10272  filint2 14923  inficlALT 15372

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430

Copyright terms: Public domain