Theorem inficl 16581

Description: A set which is closed under pairwise intersection is closed under finite intersection.

Assertion

Ref	Expression
inficl	|- ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> ( fi ` A) = A)

Distinct variable groups:   x,A,y   x,V,y

Proof of Theorem inficl

Step	Hyp	Ref	Expression
1		visset 2541	. . . . . 6 |- z e. _V
2		sppfi 11053	. . . . . 6 |- ((z e. _V /\ A e. V) -> (z e. ( fi ` A) <-> E.w(w C_ A /\ w e. Fin /\ z = |^|w)))
3	1, 2	mpan 677	. . . . 5 |- (A e. V -> (z e. ( fi ` A) <-> E.w(w C_ A /\ w e. Fin /\ z = |^|w)))
4	3	adantr 447	. . . 4 |- ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> (z e. ( fi ` A) <-> E.w(w C_ A /\ w e. Fin /\ z = |^|w)))
5		vprc 3616	. . . . . . . . . . 11 |- -. _V e. _V
6		eleq1 2204	. . . . . . . . . . . 12 |- (z = _V -> (z e. _V <-> _V e. _V))
7	1, 6	mpbii 319	. . . . . . . . . . 11 |- (z = _V -> _V e. _V)
8	5, 7	mto 151	. . . . . . . . . 10 |- -. z = _V
9		inteq 3403	. . . . . . . . . . . 12 |- (w = (/) -> |^|w = |^|(/))
10	9	eqeq2d 2152	. . . . . . . . . . 11 |- (w = (/) -> (z = |^|w <-> z = |^|(/)))
11		int0 3414	. . . . . . . . . . . 12 |- |^|(/) = _V
12		eqtr 2158	. . . . . . . . . . . 12 |- ((z = |^|(/) /\ |^|(/) = _V) -> z = _V)
13	11, 12	mpan2 679	. . . . . . . . . . 11 |- (z = |^|(/) -> z = _V)
14	10, 13	syl6bi 263	. . . . . . . . . 10 |- (w = (/) -> (z = |^|w -> z = _V))
15	8, 14	mtoi 153	. . . . . . . . 9 |- (w = (/) -> -. z = |^|w)
16	15	necon2ai 2310	. . . . . . . 8 |- (z = |^|w -> w =/= (/))
17		sseq1 2865	. . . . . . . . . . . . . . . . . 18 |- (u = (/) -> (u C_ A <-> (/) C_ A))
18		neeq1 2273	. . . . . . . . . . . . . . . . . 18 |- (u = (/) -> (u =/= (/) <-> (/) =/= (/)))
19	17, 18	anbi12d 763	. . . . . . . . . . . . . . . . 17 |- (u = (/) -> ((u C_ A /\ u =/= (/)) <-> ((/) C_ A /\ (/) =/= (/))))
20	19	anbi2d 751	. . . . . . . . . . . . . . . 16 |- (u = (/) -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) <-> ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((/) C_ A /\ (/) =/= (/)))))
21		inteq 3403	. . . . . . . . . . . . . . . . 17 |- (u = (/) -> |^|u = |^|(/))
22	21	eleq1d 2210	. . . . . . . . . . . . . . . 16 |- (u = (/) -> (|^|u e. A <-> |^|(/) e. A))
23	20, 22	imbi12d 761	. . . . . . . . . . . . . . 15 |- (u = (/) -> ((((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) -> |^|u e. A) <-> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((/) C_ A /\ (/) =/= (/))) -> |^|(/) e. A)))
24		sseq1 2865	. . . . . . . . . . . . . . . . . 18 |- (u = (v \ {z}) -> (u C_ A <-> (v \ {z}) C_ A))
25		neeq1 2273	. . . . . . . . . . . . . . . . . 18 |- (u = (v \ {z}) -> (u =/= (/) <-> (v \ {z}) =/= (/)))
26	24, 25	anbi12d 763	. . . . . . . . . . . . . . . . 17 |- (u = (v \ {z}) -> ((u C_ A /\ u =/= (/)) <-> ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))))
27	26	anbi2d 751	. . . . . . . . . . . . . . . 16 |- (u = (v \ {z}) -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) <-> ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/)))))
28		inteq 3403	. . . . . . . . . . . . . . . . 17 |- (u = (v \ {z}) -> |^|u = |^|(v \ {z}))
29	28	eleq1d 2210	. . . . . . . . . . . . . . . 16 |- (u = (v \ {z}) -> (|^|u e. A <-> |^|(v \ {z}) e. A))
30	27, 29	imbi12d 761	. . . . . . . . . . . . . . 15 |- (u = (v \ {z}) -> ((((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) -> |^|u e. A) <-> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A)))
31		sseq1 2865	. . . . . . . . . . . . . . . . . 18 |- (u = v -> (u C_ A <-> v C_ A))
32		neeq1 2273	. . . . . . . . . . . . . . . . . 18 |- (u = v -> (u =/= (/) <-> v =/= (/)))
33	31, 32	anbi12d 763	. . . . . . . . . . . . . . . . 17 |- (u = v -> ((u C_ A /\ u =/= (/)) <-> (v C_ A /\ v =/= (/))))
34	33	anbi2d 751	. . . . . . . . . . . . . . . 16 |- (u = v -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) <-> ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/)))))
35		inteq 3403	. . . . . . . . . . . . . . . . 17 |- (u = v -> |^|u = |^|v)
36	35	eleq1d 2210	. . . . . . . . . . . . . . . 16 |- (u = v -> (|^|u e. A <-> |^|v e. A))
37	34, 36	imbi12d 761	. . . . . . . . . . . . . . 15 |- (u = v -> ((((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) -> |^|u e. A) <-> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/))) -> |^|v e. A)))
38		sseq1 2865	. . . . . . . . . . . . . . . . . 18 |- (u = w -> (u C_ A <-> w C_ A))
39		neeq1 2273	. . . . . . . . . . . . . . . . . 18 |- (u = w -> (u =/= (/) <-> w =/= (/)))
40	38, 39	anbi12d 763	. . . . . . . . . . . . . . . . 17 |- (u = w -> ((u C_ A /\ u =/= (/)) <-> (w C_ A /\ w =/= (/))))
41	40	anbi2d 751	. . . . . . . . . . . . . . . 16 |- (u = w -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) <-> ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (w C_ A /\ w =/= (/)))))
42		inteq 3403	. . . . . . . . . . . . . . . . 17 |- (u = w -> |^|u = |^|w)
43	42	eleq1d 2210	. . . . . . . . . . . . . . . 16 |- (u = w -> (|^|u e. A <-> |^|w e. A))
44	41, 43	imbi12d 761	. . . . . . . . . . . . . . 15 |- (u = w -> ((((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) -> |^|u e. A) <-> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (w C_ A /\ w =/= (/))) -> |^|w e. A)))
45		eqidd 2142	. . . . . . . . . . . . . . . . 17 |- (-. |^|(/) e. A -> (/) = (/))
46	45	necon1ai 2307	. . . . . . . . . . . . . . . 16 |- ((/) =/= (/) -> |^|(/) e. A)
47	46	ad2antll 805	. . . . . . . . . . . . . . 15 |- (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((/) C_ A /\ (/) =/= (/))) -> |^|(/) e. A)
48		visset 2541	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- w e. _V
49	48	intsn 3433	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- |^|{w} = w
50	49	eleq1i 2207	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (|^|{w} e. A <-> w e. A)
51	50	biimpri 230	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w e. A -> |^|{w} e. A)
52		sseq1 2865	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v = {w} -> (v C_ A <-> {w} C_ A))
53	48	snss 3317	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w e. A <-> {w} C_ A)
54	52, 53	syl6bbr 731	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v = {w} -> (v C_ A <-> w e. A))
55		inteq 3403	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v = {w} -> |^|v = |^|{w})
56	55	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v = {w} -> (|^|v e. A <-> |^|{w} e. A))
57	54, 56	imbi12d 761	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v = {w} -> ((v C_ A -> |^|v e. A) <-> (w e. A -> |^|{w} e. A)))
58	51, 57	mpbiri 321	. . . . . . . . . . . . . . . . . . . . . 22 |- (v = {w} -> (v C_ A -> |^|v e. A))
59	58	com12 26	. . . . . . . . . . . . . . . . . . . . 21 |- (v C_ A -> (v = {w} -> |^|v e. A))
60	59	19.23adv 1860	. . . . . . . . . . . . . . . . . . . 20 |- (v C_ A -> (E.w v = {w} -> |^|v e. A))
61	60	ad2antrl 804	. . . . . . . . . . . . . . . . . . 19 |- (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/))) -> (E.w v = {w} -> |^|v e. A))
62	61	adantl 448	. . . . . . . . . . . . . . . . . 18 |- ((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/)))) -> (E.w v = {w} -> |^|v e. A))
63		n0 3091	. . . . . . . . . . . . . . . . . . . . 21 |- (v =/= (/) <-> E.u u e. v)
64		alnex 1669	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A.w -. v = {w} <-> -. E.w v = {w})
65		sneq 3247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = u -> {w} = {u})
66	65	eqeq2d 2152	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = u -> (v = {w} <-> v = {u}))
67	66	notbid 746	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = u -> (-. v = {w} <-> -. v = {u}))
68	67	a4v 1919	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.w -. v = {w} -> -. v = {u})
69		visset 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- u e. _V
70	69	snss 3317	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (u e. v <-> {u} C_ v)
71		ssdif0 3135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (v C_ {u} <-> (v \ {u}) = (/))
72		eqss 2860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (v = {u} <-> (v C_ {u} /\ {u} C_ v))
73	72	biimpri 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v C_ {u} /\ {u} C_ v) -> v = {u})
74	73	expcom 399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ({u} C_ v -> (v C_ {u} -> v = {u}))
75	71, 74	syl5bir 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ({u} C_ v -> ((v \ {u}) = (/) -> v = {u}))
76	70, 75	sylbi 225	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (u e. v -> ((v \ {u}) = (/) -> v = {u}))
77	76	necon3bd 2302	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (u e. v -> (-. v = {u} -> (v \ {u}) =/= (/)))
78	68, 77	syl5 35	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u e. v -> (A.w -. v = {w} -> (v \ {u}) =/= (/)))
79	64, 78	syl5bir 251	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u e. v -> (-. E.w v = {w} -> (v \ {u}) =/= (/)))
80	79	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ v C_ A) -> (u e. v -> (-. E.w v = {w} -> (v \ {u}) =/= (/))))
81		ssdifss 2955	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v C_ A -> (v \ {u}) C_ A)
82	81	adantl 448	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ v C_ A) -> (v \ {u}) C_ A)
83		sneq 3247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (z = u -> {z} = {u})
84	83	difeq2d 2946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (z = u -> (v \ {z}) = (v \ {u}))
85	84	sseq1d 2871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (z = u -> ((v \ {z}) C_ A <-> (v \ {u}) C_ A))
86	84	neeq1d 2278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (z = u -> ((v \ {z}) =/= (/) <-> (v \ {u}) =/= (/)))
87	85, 86	anbi12d 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (z = u -> (((v \ {z}) C_ A /\ (v \ {z}) =/= (/)) <-> ((v \ {u}) C_ A /\ (v \ {u}) =/= (/))))
88	87	anbi2d 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (z = u -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) <-> ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/)))))
89	84	inteqd 3405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (z = u -> |^|(v \ {z}) = |^|(v \ {u}))
90	89	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (z = u -> (|^|(v \ {z}) e. A <-> |^|(v \ {u}) e. A))
91	88, 90	imbi12d 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (z = u -> ((((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) <-> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/))) -> |^|(v \ {u}) e. A)))
92	91	rcla4v 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (u e. v -> (A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/))) -> |^|(v \ {u}) e. A)))
93	92	com23 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u e. v -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/))) -> (A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) -> |^|(v \ {u}) e. A)))
94		ssel 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (v C_ A -> (u e. v -> u e. A))
95	94	com12 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u e. v -> (v C_ A -> u e. A))
96		ineq1 3002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (x = |^|(v \ {u}) -> (x i^i y) = (|^|(v \ {u}) i^i y))
97	96	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (x = |^|(v \ {u}) -> ((x i^i y) e. A <-> (|^|(v \ {u}) i^i y) e. A))
98		ineq2 3003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (y = u -> (|^|(v \ {u}) i^i y) = (|^|(v \ {u}) i^i u))
99	98	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (y = u -> ((|^|(v \ {u}) i^i y) e. A <-> (|^|(v \ {u}) i^i u) e. A))
100	97, 99	rcla42v 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((|^|(v \ {u}) e. A /\ u e. A) -> (A.x e. A A.y e. A (x i^i y) e. A -> (|^|(v \ {u}) i^i u) e. A))
101		difsnid 3324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (u e. v -> ((v \ {u}) u. {u}) = v)
102	101	eqcomd 2146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (u e. v -> v = ((v \ {u}) u. {u}))
103	102	inteqd 3405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (u e. v -> |^|v = |^|((v \ {u}) u. {u}))
104	69	intunsn 3435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- |^|((v \ {u}) u. {u}) = (|^|(v \ {u}) i^i u)
105	103, 104	syl6req 2194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (u e. v -> (|^|(v \ {u}) i^i u) = |^|v)
106	105	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (u e. v -> ((|^|(v \ {u}) i^i u) e. A <-> |^|v e. A))
107	106	biimpcd 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((|^|(v \ {u}) i^i u) e. A -> (u e. v -> |^|v e. A))
108	100, 107	syl6 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((|^|(v \ {u}) e. A /\ u e. A) -> (A.x e. A A.y e. A (x i^i y) e. A -> (u e. v -> |^|v e. A)))
109	108	expcom 399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (u e. A -> (|^|(v \ {u}) e. A -> (A.x e. A A.y e. A (x i^i y) e. A -> (u e. v -> |^|v e. A))))
110	109	com4r 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u e. v -> (u e. A -> (|^|(v \ {u}) e. A -> (A.x e. A A.y e. A (x i^i y) e. A -> |^|v e. A))))
111	95, 110	syld 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (u e. v -> (v C_ A -> (|^|(v \ {u}) e. A -> (A.x e. A A.y e. A (x i^i y) e. A -> |^|v e. A))))
112	111	com24 79	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (u e. v -> (A.x e. A A.y e. A (x i^i y) e. A -> (|^|(v \ {u}) e. A -> (v C_ A -> |^|v e. A))))
113	112	adantld 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (u e. v -> ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> (|^|(v \ {u}) e. A -> (v C_ A -> |^|v e. A))))
114	113	adantrd 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u e. v -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/))) -> (|^|(v \ {u}) e. A -> (v C_ A -> |^|v e. A))))
115	93, 114	syldd 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (u e. v -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/))) -> (A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) -> (v C_ A -> |^|v e. A))))
116	115	com13 67	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/))) -> (u e. v -> (v C_ A -> |^|v e. A))))
117	116	imp 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/)))) -> (u e. v -> (v C_ A -> |^|v e. A)))
118	117	anassrs 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/))) -> (u e. v -> (v C_ A -> |^|v e. A)))
119	118	expr 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ (v \ {u}) C_ A) -> ((v \ {u}) =/= (/) -> (u e. v -> (v C_ A -> |^|v e. A))))
120	119	com24 79	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ (v \ {u}) C_ A) -> (v C_ A -> (u e. v -> ((v \ {u}) =/= (/) -> |^|v e. A))))
121	120	ex 398	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) -> ((v \ {u}) C_ A -> (v C_ A -> (u e. v -> ((v \ {u}) =/= (/) -> |^|v e. A)))))
122	121	com23 65	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) -> (v C_ A -> ((v \ {u}) C_ A -> (u e. v -> ((v \ {u}) =/= (/) -> |^|v e. A)))))
123	122	imp 393	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ v C_ A) -> ((v \ {u}) C_ A -> (u e. v -> ((v \ {u}) =/= (/) -> |^|v e. A))))
124	82, 123	mpd 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ v C_ A) -> (u e. v -> ((v \ {u}) =/= (/) -> |^|v e. A)))
125	80, 124	syldd 47	. . . . . . . . . . . . . . . . . . . . . 22 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ v C_ A) -> (u e. v -> (-. E.w v = {w} -> |^|v e. A)))
126	125	19.23adv 1860	. . . . . . . . . . . . . . . . . . . . 21 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ v C_ A) -> (E.u u e. v -> (-. E.w v = {w} -> |^|v e. A)))
127	63, 126	syl5bi 249	. . . . . . . . . . . . . . . . . . . 20 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ v C_ A) -> (v =/= (/) -> (-. E.w v = {w} -> |^|v e. A)))
128	127	impr 592	. . . . . . . . . . . . . . . . . . 19 |- (((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ (A e. V /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ (v C_ A /\ v =/= (/))) -> (-. E.w v = {w} -> |^|v e. A))
129	128	anasss 631	. . . . . . . . . . . . . . . . . 18 |- ((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/)))) -> (-. E.w v = {w} -> |^|v e. A))
130	62, 129	pm2.61d 194	. . . . . . . . . . . . . . . . 17 |- ((A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) /\ ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/)))) -> |^|v e. A)
131	130	ex 398	. . . . . . . . . . . . . . . 16 |- (A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/))) -> |^|v e. A))
132	131	a1i 8	. . . . . . . . . . . . . . 15 |- (v e. Fin -> (A.z e. v (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) -> |^|(v \ {z}) e. A) -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/))) -> |^|v e. A)))
133	23, 30, 37, 44, 47, 132	findcard 5843	. . . . . . . . . . . . . 14 |- (w e. Fin -> (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (w C_ A /\ w =/= (/))) -> |^|w e. A))
134	133	com12 26	. . . . . . . . . . . . 13 |- (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (w C_ A /\ w =/= (/))) -> (w e. Fin -> |^|w e. A))
135	134	expr 589	. . . . . . . . . . . 12 |- (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ w C_ A) -> (w =/= (/) -> (w e. Fin -> |^|w e. A)))
136	135	com23 65	. . . . . . . . . . 11 |- (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ w C_ A) -> (w e. Fin -> (w =/= (/) -> |^|w e. A)))
137	136	3impia 1314	. . . . . . . . . 10 |- (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ w C_ A /\ w e. Fin) -> (w =/= (/) -> |^|w e. A))
138		eleq1a 2213	. . . . . . . . . 10 |- (|^|w e. A -> (z = |^|w -> z e. A))
139	137, 138	syl6 42	. . . . . . . . 9 |- (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ w C_ A /\ w e. Fin) -> (w =/= (/) -> (z = |^|w -> z e. A)))
140	139	com23 65	. . . . . . . 8 |- (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ w C_ A /\ w e. Fin) -> (z = |^|w -> (w =/= (/) -> z e. A)))
141	16, 140	mpdi 98	. . . . . . 7 |- (((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) /\ w C_ A /\ w e. Fin) -> (z = |^|w -> z e. A))
142	141	3exp 1316	. . . . . 6 |- ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> (w C_ A -> (w e. Fin -> (z = |^|w -> z e. A))))
143	142	3impd 1331	. . . . 5 |- ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> ((w C_ A /\ w e. Fin /\ z = |^|w) -> z e. A))
144	143	19.23adv 1860	. . . 4 |- ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> (E.w(w C_ A /\ w e. Fin /\ z = |^|w) -> z e. A))
145	4, 144	sylbid 246	. . 3 |- ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> (z e. ( fi ` A) -> z e. A))
146	145	ssrdv 2853	. 2 |- ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> ( fi ` A) C_ A)
147		abfi2 11051	. . 3 |- (A e. V -> A C_ ( fi ` A))
148	147	adantr 447	. 2 |- ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> A C_ ( fi ` A))
149	146, 148	eqssd 2862	1 |- ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> ( fi ` A) = 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  _Vcvv 2538   \ cdif 2824   u. cun 2825   i^i cin 2826   C_ wss 2827  (/)c0 3082  {csn 3238  |^|cint 3400  ` cfv 4131  Fincfn 5587   fi cfi 11042

This theorem is referenced by:  neificl 16665

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-rab 2362  df-v 2540  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-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-1o 5344  df-er 5479  df-en 5588  df-fin 5591  df-fi 11043

Copyright terms: Public domain