Theorem elfiun 15369

Description: A finite intersection of elements taken from a union of collections.

Assertion

Ref	Expression
elfiun	|- ((B e. D /\ C e. K) -> (A e. ( fi ` (B u. C)) <-> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))

Distinct variable groups:   x,y,A   x,B,y   x,C,y   x,D,y   x,K,y

Proof of Theorem elfiun

Step	Hyp	Ref	Expression
1		elisset 2299	. . . 4 |- (A e. ( fi ` (B u. C)) -> A e. _V)
2	1	adantl 424	. . 3 |- (((B e. D /\ C e. K) /\ A e. ( fi ` (B u. C))) -> A e. _V)
3		simpll 448	. . 3 |- (((B e. D /\ C e. K) /\ A e. ( fi ` (B u. C))) -> B e. D)
4		simplr 449	. . 3 |- (((B e. D /\ C e. K) /\ A e. ( fi ` (B u. C))) -> C e. K)
5	2, 3, 4	3jca 1050	. 2 |- (((B e. D /\ C e. K) /\ A e. ( fi ` (B u. C))) -> (A e. _V /\ B e. D /\ C e. K))
6		elisset 2299	. . . . . 6 |- (A e. ( fi ` B) -> A e. _V)
7	6	3anim1i 1054	. . . . 5 |- ((A e. ( fi ` B) /\ B e. D /\ C e. K) -> (A e. _V /\ B e. D /\ C e. K))
8	7	3expib 1070	. . . 4 |- (A e. ( fi ` B) -> ((B e. D /\ C e. K) -> (A e. _V /\ B e. D /\ C e. K)))
9		elisset 2299	. . . . . 6 |- (A e. ( fi ` C) -> A e. _V)
10	9	3anim1i 1054	. . . . 5 |- ((A e. ( fi ` C) /\ B e. D /\ C e. K) -> (A e. _V /\ B e. D /\ C e. K))
11	10	3expib 1070	. . . 4 |- (A e. ( fi ` C) -> ((B e. D /\ C e. K) -> (A e. _V /\ B e. D /\ C e. K)))
12		visset 2295	. . . . . . . . . 10 |- x e. _V
13	12	inex1 3452	. . . . . . . . 9 |- (x i^i y) e. _V
14		eleq1 1957	. . . . . . . . 9 |- (A = (x i^i y) -> (A e. _V <-> (x i^i y) e. _V))
15	13, 14	mpbiri 211	. . . . . . . 8 |- (A = (x i^i y) -> A e. _V)
16	15	a1i 8	. . . . . . 7 |- ((x e. ( fi ` B) /\ y e. ( fi ` C)) -> (A = (x i^i y) -> A e. _V))
17	16	r19.23aivv 2217	. . . . . 6 |- (E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y) -> A e. _V)
18	17	3anim1i 1054	. . . . 5 |- ((E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y) /\ B e. D /\ C e. K) -> (A e. _V /\ B e. D /\ C e. K))
19	18	3expib 1070	. . . 4 |- (E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y) -> ((B e. D /\ C e. K) -> (A e. _V /\ B e. D /\ C e. K)))
20	8, 11, 19	3jaoi 1160	. . 3 |- ((A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)) -> ((B e. D /\ C e. K) -> (A e. _V /\ B e. D /\ C e. K)))
21	20	impcom 378	. 2 |- (((B e. D /\ C e. K) /\ (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))) -> (A e. _V /\ B e. D /\ C e. K))
22		sppfi 10218	. . . . 5 |- ((A e. _V /\ (B u. C) e. _V) -> (A e. ( fi ` (B u. C)) <-> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z)))
23		unexg 3798	. . . . 5 |- ((B e. D /\ C e. K) -> (B u. C) e. _V)
24	22, 23	sylan2 500	. . . 4 |- ((A e. _V /\ (B e. D /\ C e. K)) -> (A e. ( fi ` (B u. C)) <-> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z)))
25	24	3impb 1063	. . 3 |- ((A e. _V /\ B e. D /\ C e. K) -> (A e. ( fi ` (B u. C)) <-> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z)))
26		uneq12 2750	. . . . . . . . . . . 12 |- (((z i^i B) = (/) /\ (z i^i C) = (/)) -> ((z i^i B) u. (z i^i C)) = ((/) u. (/)))
27		unidm 2743	. . . . . . . . . . . 12 |- ((/) u. (/)) = (/)
28	26, 27	syl6eq 1944	. . . . . . . . . . 11 |- (((z i^i B) = (/) /\ (z i^i C) = (/)) -> ((z i^i B) u. (z i^i C)) = (/))
29	28	eqeq1d 1892	. . . . . . . . . 10 |- (((z i^i B) = (/) /\ (z i^i C) = (/)) -> (((z i^i B) u. (z i^i C)) = z <-> (/) = z))
30		inteq 3217	. . . . . . . . . . . . . . . 16 |- ((/) = z -> |^|(/) = |^|z)
31	30	eqeq2d 1895	. . . . . . . . . . . . . . 15 |- ((/) = z -> (A = |^|(/) <-> A = |^|z))
32	31	imbi1d 675	. . . . . . . . . . . . . 14 |- ((/) = z -> ((A = |^|(/) -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))) <-> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))
33		vprc 3449	. . . . . . . . . . . . . . . . 17 |- -. _V e. _V
34		int0 3230	. . . . . . . . . . . . . . . . . 18 |- |^|(/) = _V
35	34	eleq1i 1960	. . . . . . . . . . . . . . . . 17 |- (|^|(/) e. _V <-> _V e. _V)
36	33, 35	mtbir 209	. . . . . . . . . . . . . . . 16 |- -. |^|(/) e. _V
37		eleq1 1957	. . . . . . . . . . . . . . . . 17 |- (A = |^|(/) -> (A e. _V <-> |^|(/) e. _V))
38	37	biimpcd 172	. . . . . . . . . . . . . . . 16 |- (A e. _V -> (A = |^|(/) -> |^|(/) e. _V))
39	36, 38	mtoi 122	. . . . . . . . . . . . . . 15 |- (A e. _V -> -. A = |^|(/))
40	39	pm2.21d 94	. . . . . . . . . . . . . 14 |- (A e. _V -> (A = |^|(/) -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))
41	32, 40	syl5cbi 226	. . . . . . . . . . . . 13 |- (A e. _V -> ((/) = z -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))
42	41	3ad2ant1 897	. . . . . . . . . . . 12 |- ((A e. _V /\ B e. D /\ C e. K) -> ((/) = z -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))
43	42	com12 14	. . . . . . . . . . 11 |- ((/) = z -> ((A e. _V /\ B e. D /\ C e. K) -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))
44	43	a1i14 15328	. . . . . . . . . 10 |- (((z i^i B) = (/) /\ (z i^i C) = (/)) -> ((/) = z -> ((A e. _V /\ B e. D /\ C e. K) -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
45	29, 44	sylbid 220	. . . . . . . . 9 |- (((z i^i B) = (/) /\ (z i^i C) = (/)) -> (((z i^i B) u. (z i^i C)) = z -> ((A e. _V /\ B e. D /\ C e. K) -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
46	45	com23 36	. . . . . . . 8 |- (((z i^i B) = (/) /\ (z i^i C) = (/)) -> ((A e. _V /\ B e. D /\ C e. K) -> (((z i^i B) u. (z i^i C)) = z -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
47		uneq2 2749	. . . . . . . . . . . . . 14 |- ((z i^i B) = (/) -> ((z i^i C) u. (z i^i B)) = ((z i^i C) u. (/)))
48		uncom 2744	. . . . . . . . . . . . . 14 |- ((z i^i C) u. (z i^i B)) = ((z i^i B) u. (z i^i C))
49		un0 2896	. . . . . . . . . . . . . 14 |- ((z i^i C) u. (/)) = (z i^i C)
50	47, 48, 49	3eqtr3g 1952	. . . . . . . . . . . . 13 |- ((z i^i B) = (/) -> ((z i^i B) u. (z i^i C)) = (z i^i C))
51	50	adantr 425	. . . . . . . . . . . 12 |- (((z i^i B) = (/) /\ -. (z i^i C) = (/)) -> ((z i^i B) u. (z i^i C)) = (z i^i C))
52	51	eqeq1d 1892	. . . . . . . . . . 11 |- (((z i^i B) = (/) /\ -. (z i^i C) = (/)) -> (((z i^i B) u. (z i^i C)) = z <-> (z i^i C) = z))
53		df-ss 2605	. . . . . . . . . . 11 |- (z C_ C <-> (z i^i C) = z)
54	52, 53	syl6bbr 597	. . . . . . . . . 10 |- (((z i^i B) = (/) /\ -. (z i^i C) = (/)) -> (((z i^i B) u. (z i^i C)) = z <-> z C_ C))
55		eleq1 1957	. . . . . . . . . . . . . 14 |- (A = |^|z -> (A e. ( fi ` C) <-> |^|z e. ( fi ` C)))
56		simplr 449	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> z C_ C)
57		simprr 451	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> z e. Fin)
58		eqidd 1885	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> |^|z = |^|z)
59		visset 2295	. . . . . . . . . . . . . . . . 17 |- z e. _V
60		sseq1 2637	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (x C_ C <-> z C_ C))
61		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (x e. Fin <-> z e. Fin))
62		inteq 3217	. . . . . . . . . . . . . . . . . . 19 |- (x = z -> |^|x = |^|z)
63	62	eqeq2d 1895	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (|^|z = |^|x <-> |^|z = |^|z))
64	60, 61, 63	3anbi123d 1168	. . . . . . . . . . . . . . . . 17 |- (x = z -> ((x C_ C /\ x e. Fin /\ |^|z = |^|x) <-> (z C_ C /\ z e. Fin /\ |^|z = |^|z)))
65	59, 64	cla4ev 2371	. . . . . . . . . . . . . . . 16 |- ((z C_ C /\ z e. Fin /\ |^|z = |^|z) -> E.x(x C_ C /\ x e. Fin /\ |^|z = |^|x))
66	56, 57, 58, 65	syl111anc 1100	. . . . . . . . . . . . . . 15 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> E.x(x C_ C /\ x e. Fin /\ |^|z = |^|x))
67		df-ne 2019	. . . . . . . . . . . . . . . . . . 19 |- ((z i^i C) =/= (/) <-> -. (z i^i C) = (/))
68		inss1 2812	. . . . . . . . . . . . . . . . . . . 20 |- (z i^i C) C_ z
69		ssn0 2905	. . . . . . . . . . . . . . . . . . . 20 |- (((z i^i C) C_ z /\ (z i^i C) =/= (/)) -> z =/= (/))
70	68, 69	mpan 759	. . . . . . . . . . . . . . . . . . 19 |- ((z i^i C) =/= (/) -> z =/= (/))
71	67, 70	sylbir 218	. . . . . . . . . . . . . . . . . 18 |- (-. (z i^i C) = (/) -> z =/= (/))
72	71	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> z =/= (/))
73		intex 3465	. . . . . . . . . . . . . . . . 17 |- (z =/= (/) <-> |^|z e. _V)
74	72, 73	sylib 215	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> |^|z e. _V)
75		simprl3 923	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> C e. K)
76		sppfi 10218	. . . . . . . . . . . . . . . 16 |- ((|^|z e. _V /\ C e. K) -> (|^|z e. ( fi ` C) <-> E.x(x C_ C /\ x e. Fin /\ |^|z = |^|x)))
77	74, 75, 76	syl11anc 524	. . . . . . . . . . . . . . 15 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> (|^|z e. ( fi ` C) <-> E.x(x C_ C /\ x e. Fin /\ |^|z = |^|x)))
78	66, 77	mpbird 213	. . . . . . . . . . . . . 14 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> |^|z e. ( fi ` C))
79	55, 78	syl5cbir 228	. . . . . . . . . . . . 13 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> (A = |^|z -> A e. ( fi ` C)))
80		3mix2 1046	. . . . . . . . . . . . 13 |- (A e. ( fi ` C) -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))
81	79, 80	syl6 25	. . . . . . . . . . . 12 |- (((-. (z i^i C) = (/) /\ z C_ C) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))
82	81	exp43 415	. . . . . . . . . . 11 |- (-. (z i^i C) = (/) -> (z C_ C -> ((A e. _V /\ B e. D /\ C e. K) -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
83	82	adantl 424	. . . . . . . . . 10 |- (((z i^i B) = (/) /\ -. (z i^i C) = (/)) -> (z C_ C -> ((A e. _V /\ B e. D /\ C e. K) -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
84	54, 83	sylbid 220	. . . . . . . . 9 |- (((z i^i B) = (/) /\ -. (z i^i C) = (/)) -> (((z i^i B) u. (z i^i C)) = z -> ((A e. _V /\ B e. D /\ C e. K) -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
85	84	com23 36	. . . . . . . 8 |- (((z i^i B) = (/) /\ -. (z i^i C) = (/)) -> ((A e. _V /\ B e. D /\ C e. K) -> (((z i^i B) u. (z i^i C)) = z -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
86		uneq2 2749	. . . . . . . . . . . . . 14 |- ((z i^i C) = (/) -> ((z i^i B) u. (z i^i C)) = ((z i^i B) u. (/)))
87		un0 2896	. . . . . . . . . . . . . 14 |- ((z i^i B) u. (/)) = (z i^i B)
88	86, 87	syl6eq 1944	. . . . . . . . . . . . 13 |- ((z i^i C) = (/) -> ((z i^i B) u. (z i^i C)) = (z i^i B))
89	88	adantl 424	. . . . . . . . . . . 12 |- ((-. (z i^i B) = (/) /\ (z i^i C) = (/)) -> ((z i^i B) u. (z i^i C)) = (z i^i B))
90	89	eqeq1d 1892	. . . . . . . . . . 11 |- ((-. (z i^i B) = (/) /\ (z i^i C) = (/)) -> (((z i^i B) u. (z i^i C)) = z <-> (z i^i B) = z))
91		df-ss 2605	. . . . . . . . . . 11 |- (z C_ B <-> (z i^i B) = z)
92	90, 91	syl6bbr 597	. . . . . . . . . 10 |- ((-. (z i^i B) = (/) /\ (z i^i C) = (/)) -> (((z i^i B) u. (z i^i C)) = z <-> z C_ B))
93		eleq1 1957	. . . . . . . . . . . . . 14 |- (A = |^|z -> (A e. ( fi ` B) <-> |^|z e. ( fi ` B)))
94		simplr 449	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> z C_ B)
95		simprr 451	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> z e. Fin)
96		eqidd 1885	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> |^|z = |^|z)
97		sseq1 2637	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (x C_ B <-> z C_ B))
98	97, 61, 63	3anbi123d 1168	. . . . . . . . . . . . . . . . 17 |- (x = z -> ((x C_ B /\ x e. Fin /\ |^|z = |^|x) <-> (z C_ B /\ z e. Fin /\ |^|z = |^|z)))
99	59, 98	cla4ev 2371	. . . . . . . . . . . . . . . 16 |- ((z C_ B /\ z e. Fin /\ |^|z = |^|z) -> E.x(x C_ B /\ x e. Fin /\ |^|z = |^|x))
100	94, 95, 96, 99	syl111anc 1100	. . . . . . . . . . . . . . 15 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> E.x(x C_ B /\ x e. Fin /\ |^|z = |^|x))
101		df-ne 2019	. . . . . . . . . . . . . . . . . . 19 |- ((z i^i B) =/= (/) <-> -. (z i^i B) = (/))
102		inss1 2812	. . . . . . . . . . . . . . . . . . . 20 |- (z i^i B) C_ z
103		ssn0 2905	. . . . . . . . . . . . . . . . . . . 20 |- (((z i^i B) C_ z /\ (z i^i B) =/= (/)) -> z =/= (/))
104	102, 103	mpan 759	. . . . . . . . . . . . . . . . . . 19 |- ((z i^i B) =/= (/) -> z =/= (/))
105	101, 104	sylbir 218	. . . . . . . . . . . . . . . . . 18 |- (-. (z i^i B) = (/) -> z =/= (/))
106	105	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> z =/= (/))
107	106, 73	sylib 215	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> |^|z e. _V)
108		simprl2 922	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> B e. D)
109		sppfi 10218	. . . . . . . . . . . . . . . 16 |- ((|^|z e. _V /\ B e. D) -> (|^|z e. ( fi ` B) <-> E.x(x C_ B /\ x e. Fin /\ |^|z = |^|x)))
110	107, 108, 109	syl11anc 524	. . . . . . . . . . . . . . 15 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> (|^|z e. ( fi ` B) <-> E.x(x C_ B /\ x e. Fin /\ |^|z = |^|x)))
111	100, 110	mpbird 213	. . . . . . . . . . . . . 14 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> |^|z e. ( fi ` B))
112	93, 111	syl5cbir 228	. . . . . . . . . . . . 13 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> (A = |^|z -> A e. ( fi ` B)))
113		3mix1 1045	. . . . . . . . . . . . 13 |- (A e. ( fi ` B) -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))
114	112, 113	syl6 25	. . . . . . . . . . . 12 |- (((-. (z i^i B) = (/) /\ z C_ B) /\ ((A e. _V /\ B e. D /\ C e. K) /\ z e. Fin)) -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))
115	114	exp43 415	. . . . . . . . . . 11 |- (-. (z i^i B) = (/) -> (z C_ B -> ((A e. _V /\ B e. D /\ C e. K) -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
116	115	adantr 425	. . . . . . . . . 10 |- ((-. (z i^i B) = (/) /\ (z i^i C) = (/)) -> (z C_ B -> ((A e. _V /\ B e. D /\ C e. K) -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
117	92, 116	sylbid 220	. . . . . . . . 9 |- ((-. (z i^i B) = (/) /\ (z i^i C) = (/)) -> (((z i^i B) u. (z i^i C)) = z -> ((A e. _V /\ B e. D /\ C e. K) -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
118	117	com23 36	. . . . . . . 8 |- ((-. (z i^i B) = (/) /\ (z i^i C) = (/)) -> ((A e. _V /\ B e. D /\ C e. K) -> (((z i^i B) u. (z i^i C)) = z -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
119		inss2 2813	. . . . . . . . . . . . . . 15 |- (z i^i B) C_ B
120	119	a1i 8	. . . . . . . . . . . . . 14 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> (z i^i B) C_ B)
121		simprr 451	. . . . . . . . . . . . . . . 16 |- ((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) -> z e. Fin)
122	102	a1i 8	. . . . . . . . . . . . . . . 16 |- ((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) -> (z i^i B) C_ z)
123		ssfi 5630	. . . . . . . . . . . . . . . 16 |- ((z e. Fin /\ (z i^i B) C_ z) -> (z i^i B) e. Fin)
124	121, 122, 123	syl11anc 524	. . . . . . . . . . . . . . 15 |- ((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) -> (z i^i B) e. Fin)
125	124	adantr 425	. . . . . . . . . . . . . 14 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> (z i^i B) e. Fin)
126		eqidd 1885	. . . . . . . . . . . . . 14 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> |^|(z i^i B) = |^|(z i^i B))
127	59	inex1 3452	. . . . . . . . . . . . . . 15 |- (z i^i B) e. _V
128		sseq1 2637	. . . . . . . . . . . . . . . 16 |- (x = (z i^i B) -> (x C_ B <-> (z i^i B) C_ B))
129		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (x = (z i^i B) -> (x e. Fin <-> (z i^i B) e. Fin))
130		inteq 3217	. . . . . . . . . . . . . . . . 17 |- (x = (z i^i B) -> |^|x = |^|(z i^i B))
131	130	eqeq2d 1895	. . . . . . . . . . . . . . . 16 |- (x = (z i^i B) -> (|^|(z i^i B) = |^|x <-> |^|(z i^i B) = |^|(z i^i B)))
132	128, 129, 131	3anbi123d 1168	. . . . . . . . . . . . . . 15 |- (x = (z i^i B) -> ((x C_ B /\ x e. Fin /\ |^|(z i^i B) = |^|x) <-> ((z i^i B) C_ B /\ (z i^i B) e. Fin /\ |^|(z i^i B) = |^|(z i^i B))))
133	127, 132	cla4ev 2371	. . . . . . . . . . . . . 14 |- (((z i^i B) C_ B /\ (z i^i B) e. Fin /\ |^|(z i^i B) = |^|(z i^i B)) -> E.x(x C_ B /\ x e. Fin /\ |^|(z i^i B) = |^|x))
134	120, 125, 126, 133	syl111anc 1100	. . . . . . . . . . . . 13 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> E.x(x C_ B /\ x e. Fin /\ |^|(z i^i B) = |^|x))
135	101	biimpri 169	. . . . . . . . . . . . . . . . 17 |- (-. (z i^i B) = (/) -> (z i^i B) =/= (/))
136	135	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) -> (z i^i B) =/= (/))
137	136	ad2antrr 440	. . . . . . . . . . . . . . 15 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> (z i^i B) =/= (/))
138		intex 3465	. . . . . . . . . . . . . . 15 |- ((z i^i B) =/= (/) <-> |^|(z i^i B) e. _V)
139	137, 138	sylib 215	. . . . . . . . . . . . . 14 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> |^|(z i^i B) e. _V)
140		simp2 877	. . . . . . . . . . . . . . . 16 |- ((A e. _V /\ B e. D /\ C e. K) -> B e. D)
141	140	adantl 424	. . . . . . . . . . . . . . 15 |- (((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) -> B e. D)
142	141	ad2antrr 440	. . . . . . . . . . . . . 14 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> B e. D)
143		sppfi 10218	. . . . . . . . . . . . . 14 |- ((|^|(z i^i B) e. _V /\ B e. D) -> (|^|(z i^i B) e. ( fi ` B) <-> E.x(x C_ B /\ x e. Fin /\ |^|(z i^i B) = |^|x)))
144	139, 142, 143	syl11anc 524	. . . . . . . . . . . . 13 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> (|^|(z i^i B) e. ( fi ` B) <-> E.x(x C_ B /\ x e. Fin /\ |^|(z i^i B) = |^|x)))
145	134, 144	mpbird 213	. . . . . . . . . . . 12 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> |^|(z i^i B) e. ( fi ` B))
146		inss2 2813	. . . . . . . . . . . . . . 15 |- (z i^i C) C_ C
147	146	a1i 8	. . . . . . . . . . . . . 14 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> (z i^i C) C_ C)
148		ssfi 5630	. . . . . . . . . . . . . . . . 17 |- ((z e. Fin /\ (z i^i C) C_ z) -> (z i^i C) e. Fin)
149	68, 148	mpan2 760	. . . . . . . . . . . . . . . 16 |- (z e. Fin -> (z i^i C) e. Fin)
150	149	adantl 424	. . . . . . . . . . . . . . 15 |- ((((z i^i B) u. (z i^i C)) = z /\ z e. Fin) -> (z i^i C) e. Fin)
151	150	ad2antlr 441	. . . . . . . . . . . . . 14 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> (z i^i C) e. Fin)
152		eqidd 1885	. . . . . . . . . . . . . 14 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> |^|(z i^i C) = |^|(z i^i C))
153	59	inex1 3452	. . . . . . . . . . . . . . 15 |- (z i^i C) e. _V
154		sseq1 2637	. . . . . . . . . . . . . . . 16 |- (x = (z i^i C) -> (x C_ C <-> (z i^i C) C_ C))
155		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (x = (z i^i C) -> (x e. Fin <-> (z i^i C) e. Fin))
156		inteq 3217	. . . . . . . . . . . . . . . . 17 |- (x = (z i^i C) -> |^|x = |^|(z i^i C))
157	156	eqeq2d 1895	. . . . . . . . . . . . . . . 16 |- (x = (z i^i C) -> (|^|(z i^i C) = |^|x <-> |^|(z i^i C) = |^|(z i^i C)))
158	154, 155, 157	3anbi123d 1168	. . . . . . . . . . . . . . 15 |- (x = (z i^i C) -> ((x C_ C /\ x e. Fin /\ |^|(z i^i C) = |^|x) <-> ((z i^i C) C_ C /\ (z i^i C) e. Fin /\ |^|(z i^i C) = |^|(z i^i C))))
159	153, 158	cla4ev 2371	. . . . . . . . . . . . . 14 |- (((z i^i C) C_ C /\ (z i^i C) e. Fin /\ |^|(z i^i C) = |^|(z i^i C)) -> E.x(x C_ C /\ x e. Fin /\ |^|(z i^i C) = |^|x))
160	147, 151, 152, 159	syl111anc 1100	. . . . . . . . . . . . 13 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> E.x(x C_ C /\ x e. Fin /\ |^|(z i^i C) = |^|x))
161	67	biimpri 169	. . . . . . . . . . . . . . . . 17 |- (-. (z i^i C) = (/) -> (z i^i C) =/= (/))
162	161	ad2antlr 441	. . . . . . . . . . . . . . . 16 |- (((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) -> (z i^i C) =/= (/))
163	162	ad2antrr 440	. . . . . . . . . . . . . . 15 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> (z i^i C) =/= (/))
164		intex 3465	. . . . . . . . . . . . . . 15 |- ((z i^i C) =/= (/) <-> |^|(z i^i C) e. _V)
165	163, 164	sylib 215	. . . . . . . . . . . . . 14 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> |^|(z i^i C) e. _V)
166		simp3 878	. . . . . . . . . . . . . . . 16 |- ((A e. _V /\ B e. D /\ C e. K) -> C e. K)
167	166	adantl 424	. . . . . . . . . . . . . . 15 |- (((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) -> C e. K)
168	167	ad2antrr 440	. . . . . . . . . . . . . 14 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> C e. K)
169		sppfi 10218	. . . . . . . . . . . . . 14 |- ((|^|(z i^i C) e. _V /\ C e. K) -> (|^|(z i^i C) e. ( fi ` C) <-> E.x(x C_ C /\ x e. Fin /\ |^|(z i^i C) = |^|x)))
170	165, 168, 169	syl11anc 524	. . . . . . . . . . . . 13 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> (|^|(z i^i C) e. ( fi ` C) <-> E.x(x C_ C /\ x e. Fin /\ |^|(z i^i C) = |^|x)))
171	160, 170	mpbird 213	. . . . . . . . . . . 12 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> |^|(z i^i C) e. ( fi ` C))
172		inteq 3217	. . . . . . . . . . . . . . . 16 |- (((z i^i B) u. (z i^i C)) = z -> |^|((z i^i B) u. (z i^i C)) = |^|z)
173	172	eqeq2d 1895	. . . . . . . . . . . . . . 15 |- (((z i^i B) u. (z i^i C)) = z -> (A = |^|((z i^i B) u. (z i^i C)) <-> A = |^|z))
174	173	ad2antrl 442	. . . . . . . . . . . . . 14 |- ((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) -> (A = |^|((z i^i B) u. (z i^i C)) <-> A = |^|z))
175	174	biimpar 461	. . . . . . . . . . . . 13 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> A = |^|((z i^i B) u. (z i^i C)))
176		intun 3249	. . . . . . . . . . . . 13 |- |^|((z i^i B) u. (z i^i C)) = (|^|(z i^i B) i^i |^|(z i^i C))
177	175, 176	syl6eq 1944	. . . . . . . . . . . 12 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> A = (|^|(z i^i B) i^i |^|(z i^i C)))
178		ineq1 2789	. . . . . . . . . . . . . 14 |- (x = |^|(z i^i B) -> (x i^i y) = (|^|(z i^i B) i^i y))
179	178	eqeq2d 1895	. . . . . . . . . . . . 13 |- (x = |^|(z i^i B) -> (A = (x i^i y) <-> A = (|^|(z i^i B) i^i y)))
180		ineq2 2790	. . . . . . . . . . . . . 14 |- (y = |^|(z i^i C) -> (|^|(z i^i B) i^i y) = (|^|(z i^i B) i^i |^|(z i^i C)))
181	180	eqeq2d 1895	. . . . . . . . . . . . 13 |- (y = |^|(z i^i C) -> (A = (|^|(z i^i B) i^i y) <-> A = (|^|(z i^i B) i^i |^|(z i^i C))))
182	179, 181	rcla42ev 2385	. . . . . . . . . . . 12 |- ((|^|(z i^i B) e. ( fi ` B) /\ |^|(z i^i C) e. ( fi ` C) /\ A = (|^|(z i^i B) i^i |^|(z i^i C))) -> E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))
183	145, 171, 177, 182	syl111anc 1100	. . . . . . . . . . 11 |- (((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) /\ A = |^|z) -> E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))
184	183	ex 402	. . . . . . . . . 10 |- ((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) -> (A = |^|z -> E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))
185		3mix3 1047	. . . . . . . . . 10 |- (E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y) -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))
186	184, 185	syl6 25	. . . . . . . . 9 |- ((((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) /\ (A e. _V /\ B e. D /\ C e. K)) /\ (((z i^i B) u. (z i^i C)) = z /\ z e. Fin)) -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))
187	186	exp43 415	. . . . . . . 8 |- ((-. (z i^i B) = (/) /\ -. (z i^i C) = (/)) -> ((A e. _V /\ B e. D /\ C e. K) -> (((z i^i B) u. (z i^i C)) = z -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)))))))
188	46, 85, 118, 187	4cases 832	. . . . . . 7 |- ((A e. _V /\ B e. D /\ C e. K) -> (((z i^i B) u. (z i^i C)) = z -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))))
189		df-ss 2605	. . . . . . . 8 |- (z C_ (B u. C) <-> (z i^i (B u. C)) = z)
190		indi 2838	. . . . . . . . 9 |- (z i^i (B u. C)) = ((z i^i B) u. (z i^i C))
191	190	eqeq1i 1891	. . . . . . . 8 |- ((z i^i (B u. C)) = z <-> ((z i^i B) u. (z i^i C)) = z)
192	189, 191	bitri 190	. . . . . . 7 |- (z C_ (B u. C) <-> ((z i^i B) u. (z i^i C)) = z)
193	188, 192	syl5ib 223	. . . . . 6 |- ((A e. _V /\ B e. D /\ C e. K) -> (z C_ (B u. C) -> (z e. Fin -> (A = |^|z -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))))
194	193	3impd 1082	. . . . 5 |- ((A e. _V /\ B e. D /\ C e. K) -> ((z C_ (B u. C) /\ z e. Fin /\ A = |^|z) -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))
195	194	19.23adv 1584	. . . 4 |- ((A e. _V /\ B e. D /\ C e. K) -> (E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z) -> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))
196		ssun1 2767	. . . . . . . . . 10 |- B C_ (B u. C)
197		fiss 15368	. . . . . . . . . 10 |- (((B u. C) e. _V /\ B C_ (B u. C)) -> ( fi ` B) C_ ( fi ` (B u. C)))
198	196, 197	mpan2 760	. . . . . . . . 9 |- ((B u. C) e. _V -> ( fi ` B) C_ ( fi ` (B u. C)))
199	23, 198	syl 12	. . . . . . . 8 |- ((B e. D /\ C e. K) -> ( fi ` B) C_ ( fi ` (B u. C)))
200	199	3adant1 894	. . . . . . 7 |- ((A e. _V /\ B e. D /\ C e. K) -> ( fi ` B) C_ ( fi ` (B u. C)))
201	200	sseld 2619	. . . . . 6 |- ((A e. _V /\ B e. D /\ C e. K) -> (A e. ( fi ` B) -> A e. ( fi ` (B u. C))))
202		simp1 876	. . . . . . 7 |- ((A e. _V /\ B e. D /\ C e. K) -> A e. _V)
203	23	3adant1 894	. . . . . . 7 |- ((A e. _V /\ B e. D /\ C e. K) -> (B u. C) e. _V)
204	202, 203, 22	syl11anc 524	. . . . . 6 |- ((A e. _V /\ B e. D /\ C e. K) -> (A e. ( fi ` (B u. C)) <-> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z)))
205	201, 204	sylibd 219	. . . . 5 |- ((A e. _V /\ B e. D /\ C e. K) -> (A e. ( fi ` B) -> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z)))
206		ssun2 2768	. . . . . . . . . 10 |- C C_ (B u. C)
207		fiss 15368	. . . . . . . . . 10 |- (((B u. C) e. _V /\ C C_ (B u. C)) -> ( fi ` C) C_ ( fi ` (B u. C)))
208	206, 207	mpan2 760	. . . . . . . . 9 |- ((B u. C) e. _V -> ( fi ` C) C_ ( fi ` (B u. C)))
209	23, 208	syl 12	. . . . . . . 8 |- ((B e. D /\ C e. K) -> ( fi ` C) C_ ( fi ` (B u. C)))
210	209	3adant1 894	. . . . . . 7 |- ((A e. _V /\ B e. D /\ C e. K) -> ( fi ` C) C_ ( fi ` (B u. C)))
211	210	sseld 2619	. . . . . 6 |- ((A e. _V /\ B e. D /\ C e. K) -> (A e. ( fi ` C) -> A e. ( fi ` (B u. C))))
212	211, 25	sylibd 219	. . . . 5 |- ((A e. _V /\ B e. D /\ C e. K) -> (A e. ( fi ` C) -> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z)))
213		sppfi 10218	. . . . . . . . . 10 |- ((x e. _V /\ B e. D) -> (x e. ( fi ` B) <-> E.u(u C_ B /\ u e. Fin /\ x = |^|u)))
214	12, 213	mpan 759	. . . . . . . . 9 |- (B e. D -> (x e. ( fi ` B) <-> E.u(u C_ B /\ u e. Fin /\ x = |^|u)))
215	214	3ad2ant2 898	. . . . . . . 8 |- ((A e. _V /\ B e. D /\ C e. K) -> (x e. ( fi ` B) <-> E.u(u C_ B /\ u e. Fin /\ x = |^|u)))
216		visset 2295	. . . . . . . . . 10 |- y e. _V
217		sppfi 10218	. . . . . . . . . 10 |- ((y e. _V /\ C e. K) -> (y e. ( fi ` C) <-> E.v(v C_ C /\ v e. Fin /\ y = |^|v)))
218	216, 217	mpan 759	. . . . . . . . 9 |- (C e. K -> (y e. ( fi ` C) <-> E.v(v C_ C /\ v e. Fin /\ y = |^|v)))
219	218	3ad2ant3 899	. . . . . . . 8 |- ((A e. _V /\ B e. D /\ C e. K) -> (y e. ( fi ` C) <-> E.v(v C_ C /\ v e. Fin /\ y = |^|v)))
220	215, 219	anbi12d 690	. . . . . . 7 |- ((A e. _V /\ B e. D /\ C e. K) -> ((x e. ( fi ` B) /\ y e. ( fi ` C)) <-> (E.u(u C_ B /\ u e. Fin /\ x = |^|u) /\ E.v(v C_ C /\ v e. Fin /\ y = |^|v))))
221		simpl1 879	. . . . . . . . . . . . 13 |- (((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v)) -> u C_ B)
222	221	ad2antlr 441	. . . . . . . . . . . 12 |- ((((A e. _V /\ B e. D /\ C e. K) /\ ((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v))) /\ A = (x i^i y)) -> u C_ B)
223		simpr1 882	. . . . . . . . . . . . 13 |- (((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v)) -> v C_ C)
224	223	ad2antlr 441	. . . . . . . . . . . 12 |- ((((A e. _V /\ B e. D /\ C e. K) /\ ((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v))) /\ A = (x i^i y)) -> v C_ C)
225		unss12 2778	. . . . . . . . . . . 12 |- ((u C_ B /\ v C_ C) -> (u u. v) C_ (B u. C))
226	222, 224, 225	syl11anc 524	. . . . . . . . . . 11 |- ((((A e. _V /\ B e. D /\ C e. K) /\ ((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v))) /\ A = (x i^i y)) -> (u u. v) C_ (B u. C))
227		unfi 5644	. . . . . . . . . . . . . 14 |- ((u e. Fin /\ v e. Fin) -> (u u. v) e. Fin)
228	227	3ad2antr2 1042	. . . . . . . . . . . . 13 |- ((u e. Fin /\ (v C_ C /\ v e. Fin /\ y = |^|v)) -> (u u. v) e. Fin)
229	228	3ad2antl2 1039	. . . . . . . . . . . 12 |- (((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v)) -> (u u. v) e. Fin)
230	229	ad2antlr 441	. . . . . . . . . . 11 |- ((((A e. _V /\ B e. D /\ C e. K) /\ ((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v))) /\ A = (x i^i y)) -> (u u. v) e. Fin)
231		ineq12 2791	. . . . . . . . . . . . . . . . 17 |- ((x = |^|u /\ y = |^|v) -> (x i^i y) = (|^|u i^i |^|v))
232		intun 3249	. . . . . . . . . . . . . . . . 17 |- |^|(u u. v) = (|^|u i^i |^|v)
233	231, 232	syl6eqr 1946	. . . . . . . . . . . . . . . 16 |- ((x = |^|u /\ y = |^|v) -> (x i^i y) = |^|(u u. v))
234	233	3ad2antr3 1043	. . . . . . . . . . . . . . 15 |- ((x = |^|u /\ (v C_ C /\ v e. Fin /\ y = |^|v)) -> (x i^i y) = |^|(u u. v))
235	234	3ad2antl3 1040	. . . . . . . . . . . . . 14 |- (((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v)) -> (x i^i y) = |^|(u u. v))
236	235	adantl 424	. . . . . . . . . . . . 13 |- (((A e. _V /\ B e. D /\ C e. K) /\ ((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v))) -> (x i^i y) = |^|(u u. v))
237	236	eqeq2d 1895	. . . . . . . . . . . 12 |- (((A e. _V /\ B e. D /\ C e. K) /\ ((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v))) -> (A = (x i^i y) <-> A = |^|(u u. v)))
238	237	biimpa 460	. . . . . . . . . . 11 |- ((((A e. _V /\ B e. D /\ C e. K) /\ ((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v))) /\ A = (x i^i y)) -> A = |^|(u u. v))
239		visset 2295	. . . . . . . . . . . . 13 |- u e. _V
240		visset 2295	. . . . . . . . . . . . 13 |- v e. _V
241	239, 240	unex 3796	. . . . . . . . . . . 12 |- (u u. v) e. _V
242		sseq1 2637	. . . . . . . . . . . . 13 |- (z = (u u. v) -> (z C_ (B u. C) <-> (u u. v) C_ (B u. C)))
243		eleq1 1957	. . . . . . . . . . . . 13 |- (z = (u u. v) -> (z e. Fin <-> (u u. v) e. Fin))
244		inteq 3217	. . . . . . . . . . . . . 14 |- (z = (u u. v) -> |^|z = |^|(u u. v))
245	244	eqeq2d 1895	. . . . . . . . . . . . 13 |- (z = (u u. v) -> (A = |^|z <-> A = |^|(u u. v)))
246	242, 243, 245	3anbi123d 1168	. . . . . . . . . . . 12 |- (z = (u u. v) -> ((z C_ (B u. C) /\ z e. Fin /\ A = |^|z) <-> ((u u. v) C_ (B u. C) /\ (u u. v) e. Fin /\ A = |^|(u u. v))))
247	241, 246	cla4ev 2371	. . . . . . . . . . 11 |- (((u u. v) C_ (B u. C) /\ (u u. v) e. Fin /\ A = |^|(u u. v)) -> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z))
248	226, 230, 238, 247	syl111anc 1100	. . . . . . . . . 10 |- ((((A e. _V /\ B e. D /\ C e. K) /\ ((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v))) /\ A = (x i^i y)) -> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z))
249	248	exp31 407	. . . . . . . . 9 |- ((A e. _V /\ B e. D /\ C e. K) -> (((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v)) -> (A = (x i^i y) -> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z))))
250	249	19.23advv 1676	. . . . . . . 8 |- ((A e. _V /\ B e. D /\ C e. K) -> (E.uE.v((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v)) -> (A = (x i^i y) -> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z))))
251		eeanv 1707	. . . . . . . 8 |- (E.uE.v((u C_ B /\ u e. Fin /\ x = |^|u) /\ (v C_ C /\ v e. Fin /\ y = |^|v)) <-> (E.u(u C_ B /\ u e. Fin /\ x = |^|u) /\ E.v(v C_ C /\ v e. Fin /\ y = |^|v)))
252	250, 251	syl5ibr 224	. . . . . . 7 |- ((A e. _V /\ B e. D /\ C e. K) -> ((E.u(u C_ B /\ u e. Fin /\ x = |^|u) /\ E.v(v C_ C /\ v e. Fin /\ y = |^|v)) -> (A = (x i^i y) -> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z))))
253	220, 252	sylbid 220	. . . . . 6 |- ((A e. _V /\ B e. D /\ C e. K) -> ((x e. ( fi ` B) /\ y e. ( fi ` C)) -> (A = (x i^i y) -> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z))))
254	253	r19.23advv 2218	. . . . 5 |- ((A e. _V /\ B e. D /\ C e. K) -> (E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y) -> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z)))
255	205, 212, 254	3jaod 1161	. . . 4 |- ((A e. _V /\ B e. D /\ C e. K) -> ((A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y)) -> E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z)))
256	195, 255	impbid 574	. . 3 |- ((A e. _V /\ B e. D /\ C e. K) -> (E.z(z C_ (B u. C) /\ z e. Fin /\ A = |^|z) <-> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))
257	25, 256	bitrd 587	. 2 |- ((A e. _V /\ B e. D /\ C e. K) -> (A e. ( fi ` (B u. C)) <-> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))
258	5, 21, 257	pm5.21nd 744	1 |- ((B e. D /\ C e. K) -> (A e. ( fi ` (B u. C)) <-> (A e. ( fi ` B) \/ A e. ( fi ` C) \/ E.x e. ( fi ` B)E.y e. ( fi ` C)A = (x i^i y))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   \/ w3o 857   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  E.wrex 2106  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  |^|cint 3214  ` cfv 3998  Fincfn 5426   fi cfi 10210

This theorem is referenced by:  fmfnfmlem4 15597

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-oadd 5179  df-er 5318  df-en 5427  df-fin 5430  df-fi 10211

Copyright terms: Public domain