Theorem inficl 15757

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

Assertion

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

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

Proof of Theorem inficl

Step	Hyp	Ref	Expression
1		visset 2295	. . . . . 6 |- z e. _V
2		sppfi 10218	. . . . . 6 |- ((z e. _V /\ A e. B) -> (z e. ( fi ` A) <-> E.w(w C_ A /\ w e. Fin /\ z = |^|w)))
3	1, 2	mpan 759	. . . . 5 |- (A e. B -> (z e. ( fi ` A) <-> E.w(w C_ A /\ w e. Fin /\ z = |^|w)))
4	3	adantr 425	. . . 4 |- ((A e. B /\ 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 3449	. . . . . . . . . . 11 |- -. _V e. _V
6		eleq1 1957	. . . . . . . . . . . 12 |- (z = _V -> (z e. _V <-> _V e. _V))
7	1, 6	mpbii 210	. . . . . . . . . . 11 |- (z = _V -> _V e. _V)
8	5, 7	mto 121	. . . . . . . . . 10 |- -. z = _V
9		inteq 3217	. . . . . . . . . . . 12 |- (w = (/) -> |^|w = |^|(/))
10	9	eqeq2d 1895	. . . . . . . . . . 11 |- (w = (/) -> (z = |^|w <-> z = |^|(/)))
11		int0 3230	. . . . . . . . . . . 12 |- |^|(/) = _V
12		eqtr 1904	. . . . . . . . . . . 12 |- ((z = |^|(/) /\ |^|(/) = _V) -> z = _V)
13	11, 12	mpan2 760	. . . . . . . . . . 11 |- (z = |^|(/) -> z = _V)
14	10, 13	syl6bi 231	. . . . . . . . . 10 |- (w = (/) -> (z = |^|w -> z = _V))
15	8, 14	mtoi 122	. . . . . . . . 9 |- (w = (/) -> -. z = |^|w)
16	15	necon2ai 2051	. . . . . . . 8 |- (z = |^|w -> w =/= (/))
17		sseq1 2637	. . . . . . . . . . . . . . . . . 18 |- (u = (/) -> (u C_ A <-> (/) C_ A))
18		neeq1 2024	. . . . . . . . . . . . . . . . . 18 |- (u = (/) -> (u =/= (/) <-> (/) =/= (/)))
19	17, 18	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (u = (/) -> ((u C_ A /\ u =/= (/)) <-> ((/) C_ A /\ (/) =/= (/))))
20	19	anbi2d 678	. . . . . . . . . . . . . . . 16 |- (u = (/) -> (((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) <-> ((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((/) C_ A /\ (/) =/= (/)))))
21		inteq 3217	. . . . . . . . . . . . . . . . 17 |- (u = (/) -> |^|u = |^|(/))
22	21	eleq1d 1963	. . . . . . . . . . . . . . . 16 |- (u = (/) -> (|^|u e. A <-> |^|(/) e. A))
23	20, 22	imbi12d 688	. . . . . . . . . . . . . . 15 |- (u = (/) -> ((((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) -> |^|u e. A) <-> (((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((/) C_ A /\ (/) =/= (/))) -> |^|(/) e. A)))
24		sseq1 2637	. . . . . . . . . . . . . . . . . 18 |- (u = (v \ {z}) -> (u C_ A <-> (v \ {z}) C_ A))
25		neeq1 2024	. . . . . . . . . . . . . . . . . 18 |- (u = (v \ {z}) -> (u =/= (/) <-> (v \ {z}) =/= (/)))
26	24, 25	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (u = (v \ {z}) -> ((u C_ A /\ u =/= (/)) <-> ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))))
27	26	anbi2d 678	. . . . . . . . . . . . . . . 16 |- (u = (v \ {z}) -> (((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) <-> ((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/)))))
28		inteq 3217	. . . . . . . . . . . . . . . . 17 |- (u = (v \ {z}) -> |^|u = |^|(v \ {z}))
29	28	eleq1d 1963	. . . . . . . . . . . . . . . 16 |- (u = (v \ {z}) -> (|^|u e. A <-> |^|(v \ {z}) e. A))
30	27, 29	imbi12d 688	. . . . . . . . . . . . . . 15 |- (u = (v \ {z}) -> ((((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) -> |^|u e. A) <-> (((A e. B /\ 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 2637	. . . . . . . . . . . . . . . . . 18 |- (u = v -> (u C_ A <-> v C_ A))
32		neeq1 2024	. . . . . . . . . . . . . . . . . 18 |- (u = v -> (u =/= (/) <-> v =/= (/)))
33	31, 32	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (u = v -> ((u C_ A /\ u =/= (/)) <-> (v C_ A /\ v =/= (/))))
34	33	anbi2d 678	. . . . . . . . . . . . . . . 16 |- (u = v -> (((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) <-> ((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/)))))
35		inteq 3217	. . . . . . . . . . . . . . . . 17 |- (u = v -> |^|u = |^|v)
36	35	eleq1d 1963	. . . . . . . . . . . . . . . 16 |- (u = v -> (|^|u e. A <-> |^|v e. A))
37	34, 36	imbi12d 688	. . . . . . . . . . . . . . 15 |- (u = v -> ((((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) -> |^|u e. A) <-> (((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/))) -> |^|v e. A)))
38		sseq1 2637	. . . . . . . . . . . . . . . . . 18 |- (u = w -> (u C_ A <-> w C_ A))
39		neeq1 2024	. . . . . . . . . . . . . . . . . 18 |- (u = w -> (u =/= (/) <-> w =/= (/)))
40	38, 39	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (u = w -> ((u C_ A /\ u =/= (/)) <-> (w C_ A /\ w =/= (/))))
41	40	anbi2d 678	. . . . . . . . . . . . . . . 16 |- (u = w -> (((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) <-> ((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (w C_ A /\ w =/= (/)))))
42		inteq 3217	. . . . . . . . . . . . . . . . 17 |- (u = w -> |^|u = |^|w)
43	42	eleq1d 1963	. . . . . . . . . . . . . . . 16 |- (u = w -> (|^|u e. A <-> |^|w e. A))
44	41, 43	imbi12d 688	. . . . . . . . . . . . . . 15 |- (u = w -> ((((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (u C_ A /\ u =/= (/))) -> |^|u e. A) <-> (((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (w C_ A /\ w =/= (/))) -> |^|w e. A)))
45		eqidd 1885	. . . . . . . . . . . . . . . . 17 |- (-. |^|(/) e. A -> (/) = (/))
46	45	necon1ai 2047	. . . . . . . . . . . . . . . 16 |- ((/) =/= (/) -> |^|(/) e. A)
47	46	ad2antll 443	. . . . . . . . . . . . . . 15 |- (((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((/) C_ A /\ (/) =/= (/))) -> |^|(/) e. A)
48		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- w e. _V
49	48	intsn 3252	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- |^|{w} = w
50	49	eleq1i 1960	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (|^|{w} e. A <-> w e. A)
51	50	biimpri 169	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w e. A -> |^|{w} e. A)
52		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v = {w} -> (v C_ A <-> {w} C_ A))
53	48	snss 3122	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w e. A <-> {w} C_ A)
54	52, 53	syl6bbr 597	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v = {w} -> (v C_ A <-> w e. A))
55		inteq 3217	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v = {w} -> |^|v = |^|{w})
56	55	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v = {w} -> (|^|v e. A <-> |^|{w} e. A))
57	54, 56	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v = {w} -> ((v C_ A -> |^|v e. A) <-> (w e. A -> |^|{w} e. A)))
58	51, 57	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . 22 |- (v = {w} -> (v C_ A -> |^|v e. A))
59	58	com12 14	. . . . . . . . . . . . . . . . . . . . 21 |- (v C_ A -> (v = {w} -> |^|v e. A))
60	59	19.23adv 1584	. . . . . . . . . . . . . . . . . . . 20 |- (v C_ A -> (E.w v = {w} -> |^|v e. A))
61	60	ad2antrl 442	. . . . . . . . . . . . . . . . . . 19 |- (((A e. B /\ 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 424	. . . . . . . . . . . . . . . . . 18 |- ((A.z e. v (((A e. B /\ 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. B /\ 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		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- u e. _V
64	63	snss 3122	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (u e. v <-> {u} C_ v)
65		eqss 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (v = {u} <-> (v C_ {u} /\ {u} C_ v))
66	65	biimpri 169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v C_ {u} /\ {u} C_ v) -> v = {u})
67	66	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ({u} C_ v -> (v C_ {u} -> v = {u}))
68		ssdif0 2934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (v C_ {u} <-> (v \ {u}) = (/))
69	67, 68	syl5ibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ({u} C_ v -> ((v \ {u}) = (/) -> v = {u}))
70	64, 69	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (u e. v -> ((v \ {u}) = (/) -> v = {u}))
71	70	necon3bd 2039	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (u e. v -> (-. v = {u} -> (v \ {u}) =/= (/)))
72		sneq 3054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = u -> {w} = {u})
73	72	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = u -> (v = {w} <-> v = {u}))
74	73	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = u -> (-. v = {w} <-> -. v = {u}))
75	74	a4v 1649	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.w -. v = {w} -> -. v = {u})
76	71, 75	syl5 20	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u e. v -> (A.w -. v = {w} -> (v \ {u}) =/= (/)))
77		alnex 1380	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A.w -. v = {w} <-> -. E.w v = {w})
78	76, 77	syl5ibr 224	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u e. v -> (-. E.w v = {w} -> (v \ {u}) =/= (/)))
79	78	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A.z e. v (((A e. B /\ 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. B /\ 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}) =/= (/))))
80		ssdifss 2736	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v C_ A -> (v \ {u}) C_ A)
81	80	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A.z e. v (((A e. B /\ 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. B /\ A.x e. A A.y e. A (x i^i y) e. A)) /\ v C_ A) -> (v \ {u}) C_ A)
82		sneq 3054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (z = u -> {z} = {u})
83	82	difeq2d 2726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (z = u -> (v \ {z}) = (v \ {u}))
84	83	sseq1d 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (z = u -> ((v \ {z}) C_ A <-> (v \ {u}) C_ A))
85	83	neeq1d 2028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (z = u -> ((v \ {z}) =/= (/) <-> (v \ {u}) =/= (/)))
86	84, 85	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (z = u -> (((v \ {z}) C_ A /\ (v \ {z}) =/= (/)) <-> ((v \ {u}) C_ A /\ (v \ {u}) =/= (/))))
87	86	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (z = u -> (((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {z}) C_ A /\ (v \ {z}) =/= (/))) <-> ((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/)))))
88	83	inteqd 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (z = u -> |^|(v \ {z}) = |^|(v \ {u}))
89	88	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (z = u -> (|^|(v \ {z}) e. A <-> |^|(v \ {u}) e. A))
90	87, 89	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (z = u -> ((((A e. B /\ 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. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ ((v \ {u}) C_ A /\ (v \ {u}) =/= (/))) -> |^|(v \ {u}) e. A)))
91	90	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (u e. v -> (A.z e. v (((A e. B /\ 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. B /\ 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	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u e. v -> (((A e. B /\ 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. B /\ 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)))
93		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (v C_ A -> (u e. v -> u e. A))
94	93	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (u e. v -> (v C_ A -> u e. A))
95		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (x = |^|(v \ {u}) -> (x i^i y) = (|^|(v \ {u}) i^i y))
96	95	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (x = |^|(v \ {u}) -> ((x i^i y) e. A <-> (|^|(v \ {u}) i^i y) e. A))
97		ineq2 2790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (y = u -> (|^|(v \ {u}) i^i y) = (|^|(v \ {u}) i^i u))
98	97	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (y = u -> ((|^|(v \ {u}) i^i y) e. A <-> (|^|(v \ {u}) i^i u) e. A))
99	96, 98	rcla42v 2384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))
100		difsnid 3131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (u e. v -> ((v \ {u}) u. {u}) = v)
101	100	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (u e. v -> v = ((v \ {u}) u. {u}))
102	101	inteqd 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (u e. v -> |^|v = |^|((v \ {u}) u. {u}))
103	63	intunsn 3254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- |^|((v \ {u}) u. {u}) = (|^|(v \ {u}) i^i u)
104	102, 103	syl6req 1945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (u e. v -> (|^|(v \ {u}) i^i u) = |^|v)
105	104	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (u e. v -> ((|^|(v \ {u}) i^i u) e. A <-> |^|v e. A))
106	105	biimpcd 172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((|^|(v \ {u}) i^i u) e. A -> (u e. v -> |^|v e. A))
107	99, 106	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))
108	107	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
109	108	com4r 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
110	94, 109	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
111	110	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))
112	111	adantld 426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (u e. v -> ((A e. B /\ 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	adantrd 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u e. v -> (((A e. B /\ 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))))
114	92, 113	syldd 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (u e. v -> (((A e. B /\ 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. B /\ 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))))
115	114	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A.z e. v (((A e. B /\ 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. B /\ 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))))
116	115	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((A.z e. v (((A e. B /\ 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. B /\ 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	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((A.z e. v (((A e. B /\ 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. B /\ 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	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((A.z e. v (((A e. B /\ 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. B /\ 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	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((A.z e. v (((A e. B /\ 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. B /\ 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))))
120	119	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A.z e. v (((A e. B /\ 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. B /\ 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	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.z e. v (((A e. B /\ 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. B /\ 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)))))
122	121	imp 377	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A.z e. v (((A e. B /\ 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. B /\ 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	81, 122	mpd 29	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A.z e. v (((A e. B /\ 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. B /\ 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)))
124	79, 123	syldd 61	. . . . . . . . . . . . . . . . . . . . . 22 |- (((A.z e. v (((A e. B /\ 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. B /\ 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)))
125	124	19.23adv 1584	. . . . . . . . . . . . . . . . . . . . 21 |- (((A.z e. v (((A e. B /\ 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. B /\ 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)))
126		n0 2884	. . . . . . . . . . . . . . . . . . . . 21 |- (v =/= (/) <-> E.u u e. v)
127	125, 126	syl5ib 223	. . . . . . . . . . . . . . . . . . . 20 |- (((A.z e. v (((A e. B /\ 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. B /\ 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 422	. . . . . . . . . . . . . . . . . . 19 |- (((A.z e. v (((A e. B /\ 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. B /\ 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 488	. . . . . . . . . . . . . . . . . 18 |- ((A.z e. v (((A e. B /\ 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. B /\ 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 141	. . . . . . . . . . . . . . . . 17 |- ((A.z e. v (((A e. B /\ 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. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (v C_ A /\ v =/= (/)))) -> |^|v e. A)
131	130	ex 402	. . . . . . . . . . . . . . . 16 |- (A.z e. v (((A e. B /\ 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. B /\ 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. B /\ 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. B /\ 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 10178	. . . . . . . . . . . . . 14 |- (w e. Fin -> (((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) /\ (w C_ A /\ w =/= (/))) -> |^|w e. A))
134	133	com12 14	. . . . . . . . . . . . 13 |- (((A e. B /\ 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 418	. . . . . . . . . . . 12 |- (((A e. B /\ 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 36	. . . . . . . . . . 11 |- (((A e. B /\ 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 1064	. . . . . . . . . 10 |- (((A e. B /\ 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 1966	. . . . . . . . . 10 |- (|^|w e. A -> (z = |^|w -> z e. A))
139	137, 138	syl6 25	. . . . . . . . 9 |- (((A e. B /\ 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 36	. . . . . . . 8 |- (((A e. B /\ 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 59	. . . . . . 7 |- (((A e. B /\ 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 1066	. . . . . 6 |- ((A e. B /\ 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 1082	. . . . 5 |- ((A e. B /\ 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 1584	. . . 4 |- ((A e. B /\ 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 220	. . 3 |- ((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) -> (z e. ( fi ` A) -> z e. A))
146	145	ssrdv 2622	. 2 |- ((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) -> ( fi ` A) C_ A)
147		abfi2 10216	. . 3 |- (A e. B -> A C_ ( fi ` A))
148	147	adantr 425	. 2 |- ((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) -> A C_ ( fi ` A))
149	146, 148	eqssd 2633	1 |- ((A e. B /\ A.x e. A A.y e. A (x i^i y) e. A) -> ( fi ` A) = 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  _Vcvv 2292   \ cdif 2590   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  |^|cint 3214  ` cfv 3998  Fincfn 5426   fi cfi 10210

This theorem is referenced by:  neificl 15841

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-rab 2112  df-v 2294  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-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-1o 5177  df-er 5318  df-en 5427  df-fin 5430  df-fi 10211

Copyright terms: Public domain