Theorem nnpweq 4524

Description: If two sets are the same finite size, then so are their power classes. Theorem X.1.41 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)

Assertion

Ref	Expression
nnpweq	|- ((M e. Nn /\ A e. M /\ B e. M) -> E.n e. Nn (~PA e. n /\ ~PB e. n))

Distinct variable groups:   A,n   B,n   n,M

Proof of Theorem nnpweq

Dummy variables a b c d e f x y m j k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnpweqlem1 4523	. . . 4 |- {m | A.a e. m A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n)} e. _V
2		raleq 2808	. . . . . 6 |- (m = 0c -> (A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
3	2	raleqbi1dv 2816	. . . . 5 |- (m = 0c -> (A.a e. m A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.a e. 0c A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
4		df-ral 2620	. . . . . 6 |- (A.a e. 0c A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.a(a e. 0c -> A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
5		el0c 4422	. . . . . . . 8 |- (a e. 0c <-> a = (/))
6	5	imbi1i 315	. . . . . . 7 |- ((a e. 0c -> A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n)) <-> (a = (/) -> A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
7	6	albii 1566	. . . . . 6 |- (A.a(a e. 0c -> A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n)) <-> A.a(a = (/) -> A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
8		0ex 4111	. . . . . . . 8 |- (/) e. _V
9		pweq 3726	. . . . . . . . . . . . 13 |- (a = (/) -> ~Pa = ~P(/))
10		pw0 4161	. . . . . . . . . . . . 13 |- ~P(/) = {(/)}
11	9, 10	syl6eq 2401	. . . . . . . . . . . 12 |- (a = (/) -> ~Pa = {(/)})
12	11	eleq1d 2419	. . . . . . . . . . 11 |- (a = (/) -> (~Pa e. n <-> {(/)} e. n))
13	12	anbi1d 685	. . . . . . . . . 10 |- (a = (/) -> ((~Pa e. n /\ ~Pb e. n) <-> ({(/)} e. n /\ ~Pb e. n)))
14	13	rexbidv 2636	. . . . . . . . 9 |- (a = (/) -> (E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> E.n e. Nn ({(/)} e. n /\ ~Pb e. n)))
15	14	ralbidv 2635	. . . . . . . 8 |- (a = (/) -> (A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.b e. 0c E.n e. Nn ({(/)} e. n /\ ~Pb e. n)))
16	8, 15	ceqsalv 2886	. . . . . . 7 |- (A.a(a = (/) -> A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n)) <-> A.b e. 0c E.n e. Nn ({(/)} e. n /\ ~Pb e. n))
17		df-ral 2620	. . . . . . . 8 |- (A.b e. 0c E.n e. Nn ({(/)} e. n /\ ~Pb e. n) <-> A.b(b e. 0c -> E.n e. Nn ({(/)} e. n /\ ~Pb e. n)))
18		el0c 4422	. . . . . . . . . 10 |- (b e. 0c <-> b = (/))
19	18	imbi1i 315	. . . . . . . . 9 |- ((b e. 0c -> E.n e. Nn ({(/)} e. n /\ ~Pb e. n)) <-> (b = (/) -> E.n e. Nn ({(/)} e. n /\ ~Pb e. n)))
20	19	albii 1566	. . . . . . . 8 |- (A.b(b e. 0c -> E.n e. Nn ({(/)} e. n /\ ~Pb e. n)) <-> A.b(b = (/) -> E.n e. Nn ({(/)} e. n /\ ~Pb e. n)))
21	17, 20	bitri 240	. . . . . . 7 |- (A.b e. 0c E.n e. Nn ({(/)} e. n /\ ~Pb e. n) <-> A.b(b = (/) -> E.n e. Nn ({(/)} e. n /\ ~Pb e. n)))
22		pweq 3726	. . . . . . . . . . . . 13 |- (b = (/) -> ~Pb = ~P(/))
23	22, 10	syl6eq 2401	. . . . . . . . . . . 12 |- (b = (/) -> ~Pb = {(/)})
24	23	eleq1d 2419	. . . . . . . . . . 11 |- (b = (/) -> (~Pb e. n <-> {(/)} e. n))
25	24	anbi2d 684	. . . . . . . . . 10 |- (b = (/) -> (({(/)} e. n /\ ~Pb e. n) <-> ({(/)} e. n /\ {(/)} e. n)))
26		anidm 625	. . . . . . . . . 10 |- (({(/)} e. n /\ {(/)} e. n) <-> {(/)} e. n)
27	25, 26	syl6bb 252	. . . . . . . . 9 |- (b = (/) -> (({(/)} e. n /\ ~Pb e. n) <-> {(/)} e. n))
28	27	rexbidv 2636	. . . . . . . 8 |- (b = (/) -> (E.n e. Nn ({(/)} e. n /\ ~Pb e. n) <-> E.n e. Nn {(/)} e. n))
29	8, 28	ceqsalv 2886	. . . . . . 7 |- (A.b(b = (/) -> E.n e. Nn ({(/)} e. n /\ ~Pb e. n)) <-> E.n e. Nn {(/)} e. n)
30	16, 21, 29	3bitri 262	. . . . . 6 |- (A.a(a = (/) -> A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n)) <-> E.n e. Nn {(/)} e. n)
31	4, 7, 30	3bitri 262	. . . . 5 |- (A.a e. 0c A.b e. 0c E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> E.n e. Nn {(/)} e. n)
32	3, 31	syl6bb 252	. . . 4 |- (m = 0c -> (A.a e. m A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> E.n e. Nn {(/)} e. n))
33		raleq 2808	. . . . 5 |- (m = k -> (A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
34	33	raleqbi1dv 2816	. . . 4 |- (m = k -> (A.a e. m A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.a e. k A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
35		raleq 2808	. . . . . 6 |- (m = (k +o 1c) -> (A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.b e. (k +o 1c)E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
36	35	raleqbi1dv 2816	. . . . 5 |- (m = (k +o 1c) -> (A.a e. m A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.a e. (k +o 1c)A.b e. (k +o 1c)E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
37		pweq 3726	. . . . . . . . . 10 |- (a = c -> ~Pa = ~Pc)
38	37	eleq1d 2419	. . . . . . . . 9 |- (a = c -> (~Pa e. n <-> ~Pc e. n))
39	38	anbi1d 685	. . . . . . . 8 |- (a = c -> ((~Pa e. n /\ ~Pb e. n) <-> (~Pc e. n /\ ~Pb e. n)))
40	39	rexbidv 2636	. . . . . . 7 |- (a = c -> (E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> E.n e. Nn (~Pc e. n /\ ~Pb e. n)))
41		pweq 3726	. . . . . . . . . 10 |- (b = d -> ~Pb = ~Pd)
42	41	eleq1d 2419	. . . . . . . . 9 |- (b = d -> (~Pb e. n <-> ~Pd e. n))
43	42	anbi2d 684	. . . . . . . 8 |- (b = d -> ((~Pc e. n /\ ~Pb e. n) <-> (~Pc e. n /\ ~Pd e. n)))
44	43	rexbidv 2636	. . . . . . 7 |- (b = d -> (E.n e. Nn (~Pc e. n /\ ~Pb e. n) <-> E.n e. Nn (~Pc e. n /\ ~Pd e. n)))
45	40, 44	cbvral2v 2844	. . . . . 6 |- (A.a e. (k +o 1c)A.b e. (k +o 1c)E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.c e. (k +o 1c)A.d e. (k +o 1c)E.n e. Nn (~Pc e. n /\ ~Pd e. n))
46		eleq2 2414	. . . . . . . . 9 |- (n = j -> (~Pc e. n <-> ~Pc e. j))
47		eleq2 2414	. . . . . . . . 9 |- (n = j -> (~Pd e. n <-> ~Pd e. j))
48	46, 47	anbi12d 691	. . . . . . . 8 |- (n = j -> ((~Pc e. n /\ ~Pd e. n) <-> (~Pc e. j /\ ~Pd e. j)))
49	48	cbvrexv 2837	. . . . . . 7 |- (E.n e. Nn (~Pc e. n /\ ~Pd e. n) <-> E.j e. Nn (~Pc e. j /\ ~Pd e. j))
50	49	2ralbii 2641	. . . . . 6 |- (A.c e. (k +o 1c)A.d e. (k +o 1c)E.n e. Nn (~Pc e. n /\ ~Pd e. n) <-> A.c e. (k +o 1c)A.d e. (k +o 1c)E.j e. Nn (~Pc e. j /\ ~Pd e. j))
51	45, 50	bitri 240	. . . . 5 |- (A.a e. (k +o 1c)A.b e. (k +o 1c)E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.c e. (k +o 1c)A.d e. (k +o 1c)E.j e. Nn (~Pc e. j /\ ~Pd e. j))
52	36, 51	syl6bb 252	. . . 4 |- (m = (k +o 1c) -> (A.a e. m A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.c e. (k +o 1c)A.d e. (k +o 1c)E.j e. Nn (~Pc e. j /\ ~Pd e. j)))
53		raleq 2808	. . . . 5 |- (m = M -> (A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.b e. M E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
54	53	raleqbi1dv 2816	. . . 4 |- (m = M -> (A.a e. m A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> A.a e. M A.b e. M E.n e. Nn (~Pa e. n /\ ~Pb e. n)))
55		1cnnc 4409	. . . . 5 |- 1c e. Nn
56	8	snel1c 4141	. . . . 5 |- {(/)} e. 1c
57		eleq2 2414	. . . . . 6 |- (n = 1c -> ({(/)} e. n <-> {(/)} e. 1c))
58	57	rspcev 2956	. . . . 5 |- ((1c e. Nn /\ {(/)} e. 1c) -> E.n e. Nn {(/)} e. n)
59	55, 56, 58	mp2an 653	. . . 4 |- E.n e. Nn {(/)} e. n
60		reeanv 2779	. . . . . . . 8 |- (E.e e. k E.f e. k (E.x e. ∼ ec = (e u. {x}) /\ E.y e. ∼ fd = (f u. {y})) <-> (E.e e. k E.x e. ∼ ec = (e u. {x}) /\ E.f e. k E.y e. ∼ fd = (f u. {y})))
61		reeanv 2779	. . . . . . . . 9 |- (E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})) <-> (E.x e. ∼ ec = (e u. {x}) /\ E.y e. ∼ fd = (f u. {y})))
62	61	2rexbii 2642	. . . . . . . 8 |- (E.e e. k E.f e. k E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})) <-> E.e e. k E.f e. k (E.x e. ∼ ec = (e u. {x}) /\ E.y e. ∼ fd = (f u. {y})))
63		elsuc 4414	. . . . . . . . 9 |- (c e. (k +o 1c) <-> E.e e. k E.x e. ∼ ec = (e u. {x}))
64		elsuc 4414	. . . . . . . . 9 |- (d e. (k +o 1c) <-> E.f e. k E.y e. ∼ fd = (f u. {y}))
65	63, 64	anbi12i 678	. . . . . . . 8 |- ((c e. (k +o 1c) /\ d e. (k +o 1c)) <-> (E.e e. k E.x e. ∼ ec = (e u. {x}) /\ E.f e. k E.y e. ∼ fd = (f u. {y})))
66	60, 62, 65	3bitr4ri 269	. . . . . . 7 |- ((c e. (k +o 1c) /\ d e. (k +o 1c)) <-> E.e e. k E.f e. k E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})))
67		pweq 3726	. . . . . . . . . . . . . . . 16 |- (a = e -> ~Pa = ~Pe)
68	67	eleq1d 2419	. . . . . . . . . . . . . . 15 |- (a = e -> (~Pa e. n <-> ~Pe e. n))
69	68	anbi1d 685	. . . . . . . . . . . . . 14 |- (a = e -> ((~Pa e. n /\ ~Pb e. n) <-> (~Pe e. n /\ ~Pb e. n)))
70	69	rexbidv 2636	. . . . . . . . . . . . 13 |- (a = e -> (E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> E.n e. Nn (~Pe e. n /\ ~Pb e. n)))
71		pweq 3726	. . . . . . . . . . . . . . . 16 |- (b = f -> ~Pb = ~Pf)
72	71	eleq1d 2419	. . . . . . . . . . . . . . 15 |- (b = f -> (~Pb e. n <-> ~Pf e. n))
73	72	anbi2d 684	. . . . . . . . . . . . . 14 |- (b = f -> ((~Pe e. n /\ ~Pb e. n) <-> (~Pe e. n /\ ~Pf e. n)))
74	73	rexbidv 2636	. . . . . . . . . . . . 13 |- (b = f -> (E.n e. Nn (~Pe e. n /\ ~Pb e. n) <-> E.n e. Nn (~Pe e. n /\ ~Pf e. n)))
75	70, 74	rspc2v 2962	. . . . . . . . . . . 12 |- ((e e. k /\ f e. k) -> (A.a e. k A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n) -> E.n e. Nn (~Pe e. n /\ ~Pf e. n)))
76	75	adantl 452	. . . . . . . . . . 11 |- ((k e. Nn /\ (e e. k /\ f e. k)) -> (A.a e. k A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n) -> E.n e. Nn (~Pe e. n /\ ~Pf e. n)))
77		nncaddccl 4420	. . . . . . . . . . . . . . . . . . . . 21 |- ((n e. Nn /\ n e. Nn ) -> (n +o n) e. Nn )
78	77	anidms 626	. . . . . . . . . . . . . . . . . . . 20 |- (n e. Nn -> (n +o n) e. Nn )
79	78	adantl 452	. . . . . . . . . . . . . . . . . . 19 |- ((k e. Nn /\ n e. Nn ) -> (n +o n) e. Nn )
80	79	3ad2ant1 976	. . . . . . . . . . . . . . . . . 18 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> (n +o n) e. Nn )
81		simp1l 979	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> k e. Nn )
82		simp1r 980	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> n e. Nn )
83		simp2ll 1022	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> e e. k)
84		simp3l 983	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> x e. ∼ e)
85		simp2rl 1024	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> ~Pe e. n)
86		nnadjoinpw 4522	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ n e. Nn ) /\ (e e. k /\ x e. ∼ e) /\ ~Pe e. n) -> ~P(e u. {x}) e. (n +o n))
87	81, 82, 83, 84, 85, 86	syl221anc 1193	. . . . . . . . . . . . . . . . . 18 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> ~P(e u. {x}) e. (n +o n))
88		simp2lr 1023	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> f e. k)
89		simp3r 984	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> y e. ∼ f)
90		simp2rr 1025	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> ~Pf e. n)
91		nnadjoinpw 4522	. . . . . . . . . . . . . . . . . . 19 |- (((k e. Nn /\ n e. Nn ) /\ (f e. k /\ y e. ∼ f) /\ ~Pf e. n) -> ~P(f u. {y}) e. (n +o n))
92	81, 82, 88, 89, 90, 91	syl221anc 1193	. . . . . . . . . . . . . . . . . 18 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> ~P(f u. {y}) e. (n +o n))
93		eleq2 2414	. . . . . . . . . . . . . . . . . . . 20 |- (j = (n +o n) -> (~P(e u. {x}) e. j <-> ~P(e u. {x}) e. (n +o n)))
94		eleq2 2414	. . . . . . . . . . . . . . . . . . . 20 |- (j = (n +o n) -> (~P(f u. {y}) e. j <-> ~P(f u. {y}) e. (n +o n)))
95	93, 94	anbi12d 691	. . . . . . . . . . . . . . . . . . 19 |- (j = (n +o n) -> ((~P(e u. {x}) e. j /\ ~P(f u. {y}) e. j) <-> (~P(e u. {x}) e. (n +o n) /\ ~P(f u. {y}) e. (n +o n))))
96	95	rspcev 2956	. . . . . . . . . . . . . . . . . 18 |- (((n +o n) e. Nn /\ (~P(e u. {x}) e. (n +o n) /\ ~P(f u. {y}) e. (n +o n))) -> E.j e. Nn (~P(e u. {x}) e. j /\ ~P(f u. {y}) e. j))
97	80, 87, 92, 96	syl12anc 1180	. . . . . . . . . . . . . . . . 17 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> E.j e. Nn (~P(e u. {x}) e. j /\ ~P(f u. {y}) e. j))
98		pweq 3726	. . . . . . . . . . . . . . . . . . . 20 |- (c = (e u. {x}) -> ~Pc = ~P(e u. {x}))
99	98	eleq1d 2419	. . . . . . . . . . . . . . . . . . 19 |- (c = (e u. {x}) -> (~Pc e. j <-> ~P(e u. {x}) e. j))
100		pweq 3726	. . . . . . . . . . . . . . . . . . . 20 |- (d = (f u. {y}) -> ~Pd = ~P(f u. {y}))
101	100	eleq1d 2419	. . . . . . . . . . . . . . . . . . 19 |- (d = (f u. {y}) -> (~Pd e. j <-> ~P(f u. {y}) e. j))
102	99, 101	bi2anan9 843	. . . . . . . . . . . . . . . . . 18 |- ((c = (e u. {x}) /\ d = (f u. {y})) -> ((~Pc e. j /\ ~Pd e. j) <-> (~P(e u. {x}) e. j /\ ~P(f u. {y}) e. j)))
103	102	rexbidv 2636	. . . . . . . . . . . . . . . . 17 |- ((c = (e u. {x}) /\ d = (f u. {y})) -> (E.j e. Nn (~Pc e. j /\ ~Pd e. j) <-> E.j e. Nn (~P(e u. {x}) e. j /\ ~P(f u. {y}) e. j)))
104	97, 103	syl5ibrcom 213	. . . . . . . . . . . . . . . 16 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n)) /\ (x e. ∼ e /\ y e. ∼ f)) -> ((c = (e u. {x}) /\ d = (f u. {y})) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j)))
105	104	3expia 1153	. . . . . . . . . . . . . . 15 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n))) -> ((x e. ∼ e /\ y e. ∼ f) -> ((c = (e u. {x}) /\ d = (f u. {y})) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j))))
106	105	rexlimdvv 2745	. . . . . . . . . . . . . 14 |- (((k e. Nn /\ n e. Nn ) /\ ((e e. k /\ f e. k) /\ (~Pe e. n /\ ~Pf e. n))) -> (E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j)))
107	106	expr 598	. . . . . . . . . . . . 13 |- (((k e. Nn /\ n e. Nn ) /\ (e e. k /\ f e. k)) -> ((~Pe e. n /\ ~Pf e. n) -> (E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j))))
108	107	an32s 779	. . . . . . . . . . . 12 |- (((k e. Nn /\ (e e. k /\ f e. k)) /\ n e. Nn ) -> ((~Pe e. n /\ ~Pf e. n) -> (E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j))))
109	108	rexlimdva 2739	. . . . . . . . . . 11 |- ((k e. Nn /\ (e e. k /\ f e. k)) -> (E.n e. Nn (~Pe e. n /\ ~Pf e. n) -> (E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j))))
110	76, 109	syld 40	. . . . . . . . . 10 |- ((k e. Nn /\ (e e. k /\ f e. k)) -> (A.a e. k A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n) -> (E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j))))
111	110	imp 418	. . . . . . . . 9 |- (((k e. Nn /\ (e e. k /\ f e. k)) /\ A.a e. k A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n)) -> (E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j)))
112	111	an32s 779	. . . . . . . 8 |- (((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n)) /\ (e e. k /\ f e. k)) -> (E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j)))
113	112	rexlimdvva 2746	. . . . . . 7 |- ((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n)) -> (E.e e. k E.f e. k E.x e. ∼ eE.y e. ∼ f(c = (e u. {x}) /\ d = (f u. {y})) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j)))
114	66, 113	syl5bi 208	. . . . . 6 |- ((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n)) -> ((c e. (k +o 1c) /\ d e. (k +o 1c)) -> E.j e. Nn (~Pc e. j /\ ~Pd e. j)))
115	114	ralrimivv 2706	. . . . 5 |- ((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n)) -> A.c e. (k +o 1c)A.d e. (k +o 1c)E.j e. Nn (~Pc e. j /\ ~Pd e. j))
116	115	ex 423	. . . 4 |- (k e. Nn -> (A.a e. k A.b e. k E.n e. Nn (~Pa e. n /\ ~Pb e. n) -> A.c e. (k +o 1c)A.d e. (k +o 1c)E.j e. Nn (~Pc e. j /\ ~Pd e. j)))
117	1, 32, 34, 52, 54, 59, 116	finds 4412	. . 3 |- (M e. Nn -> A.a e. M A.b e. M E.n e. Nn (~Pa e. n /\ ~Pb e. n))
118		pweq 3726	. . . . . . 7 |- (a = A -> ~Pa = ~PA)
119	118	eleq1d 2419	. . . . . 6 |- (a = A -> (~Pa e. n <-> ~PA e. n))
120	119	anbi1d 685	. . . . 5 |- (a = A -> ((~Pa e. n /\ ~Pb e. n) <-> (~PA e. n /\ ~Pb e. n)))
121	120	rexbidv 2636	. . . 4 |- (a = A -> (E.n e. Nn (~Pa e. n /\ ~Pb e. n) <-> E.n e. Nn (~PA e. n /\ ~Pb e. n)))
122		pweq 3726	. . . . . . 7 |- (b = B -> ~Pb = ~PB)
123	122	eleq1d 2419	. . . . . 6 |- (b = B -> (~Pb e. n <-> ~PB e. n))
124	123	anbi2d 684	. . . . 5 |- (b = B -> ((~PA e. n /\ ~Pb e. n) <-> (~PA e. n /\ ~PB e. n)))
125	124	rexbidv 2636	. . . 4 |- (b = B -> (E.n e. Nn (~PA e. n /\ ~Pb e. n) <-> E.n e. Nn (~PA e. n /\ ~PB e. n)))
126	121, 125	rspc2v 2962	. . 3 |- ((A e. M /\ B e. M) -> (A.a e. M A.b e. M E.n e. Nn (~Pa e. n /\ ~Pb e. n) -> E.n e. Nn (~PA e. n /\ ~PB e. n)))
127	117, 126	syl5com 26	. 2 |- (M e. Nn -> ((A e. M /\ B e. M) -> E.n e. Nn (~PA e. n /\ ~PB e. n)))
128	127	3impib 1149	1 |- ((M e. Nn /\ A e. M /\ B e. M) -> E.n e. Nn (~PA e. n /\ ~PB e. n))

Syntax hints:   -> wi 4   /\ wa 358   /\ w3a 934  A.wal 1540   = wceq 1642   e. wcel 1710  A.wral 2615  E.wrex 2616   ∼ ccompl 3206   u. cun 3208  (/)c0 3551  ~Pcpw 3723  {csn 3738  1_cc1c 4135   Nn cnnc 4374  0_cc0c 4375   +o cplc 4376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-0c 4378  df-addc 4379  df-nnc 4380

This theorem is referenced by:  sfin112  4530  sfindbl  4531  sfinltfin  4536