Theorem ncfinraise 4481

Description: If two sets are in a particular finite cardinal, then their unit power sets are in the same natural. Theorem X.1.25 of [Rosser] p. 527. (Contributed by SF, 21-Jan-2015.)

Assertion

Ref	Expression
ncfinraise	|- ((M e. Nn /\ A e. M /\ B e. M) -> E.n e. Nn (~P1 A e. n /\ ~P1 B e. n))

Distinct variable groups:   A,n   B,n

Allowed substitution hint:   M(n)

Proof of Theorem ncfinraise

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

Step	Hyp	Ref	Expression
1		ncfinraiselem2 4480	. . . 4 |- {m | A.a e. m A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)} e. _V
2		raleq 2807	. . . . 5 |- (m = 0c -> (A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> A.b e. 0c E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
3	2	raleqbi1dv 2815	. . . 4 |- (m = 0c -> (A.a e. m A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> A.a e. 0c A.b e. 0c E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
4		raleq 2807	. . . . 5 |- (m = k -> (A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
5	4	raleqbi1dv 2815	. . . 4 |- (m = k -> (A.a e. m A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
6		raleq 2807	. . . . 5 |- (m = (k +o 1c) -> (A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> A.b e. (k +o 1c)E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
7	6	raleqbi1dv 2815	. . . 4 |- (m = (k +o 1c) -> (A.a e. m A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> A.a e. (k +o 1c)A.b e. (k +o 1c)E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
8		raleq 2807	. . . . 5 |- (m = M -> (A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> A.b e. M E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
9	8	raleqbi1dv 2815	. . . 4 |- (m = M -> (A.a e. m A.b e. m E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> A.a e. M A.b e. M E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
10		el0c 4421	. . . . . 6 |- (a e. 0c <-> a = (/))
11		el0c 4421	. . . . . 6 |- (b e. 0c <-> b = (/))
12		peano1 4402	. . . . . . . 8 |- 0c e. Nn
13		nulel0c 4422	. . . . . . . . 9 |- (/) e. 0c
14	13, 13	pm3.2i 441	. . . . . . . 8 |- ((/) e. 0c /\ (/) e. 0c)
15		eleq2 2414	. . . . . . . . . 10 |- (n = 0c -> ((/) e. n <-> (/) e. 0c))
16	15, 15	anbi12d 691	. . . . . . . . 9 |- (n = 0c -> (((/) e. n /\ (/) e. n) <-> ((/) e. 0c /\ (/) e. 0c)))
17	16	rspcev 2955	. . . . . . . 8 |- ((0c e. Nn /\ ((/) e. 0c /\ (/) e. 0c)) -> E.n e. Nn ((/) e. n /\ (/) e. n))
18	12, 14, 17	mp2an 653	. . . . . . 7 |- E.n e. Nn ((/) e. n /\ (/) e. n)
19		pw1eq 4143	. . . . . . . . . . 11 |- (a = (/) -> ~P1 a = ~P1 (/))
20		pw10 4161	. . . . . . . . . . 11 |- ~P1 (/) = (/)
21	19, 20	syl6eq 2401	. . . . . . . . . 10 |- (a = (/) -> ~P1 a = (/))
22	21	eleq1d 2419	. . . . . . . . 9 |- (a = (/) -> (~P1 a e. n <-> (/) e. n))
23		pw1eq 4143	. . . . . . . . . . 11 |- (b = (/) -> ~P1 b = ~P1 (/))
24	23, 20	syl6eq 2401	. . . . . . . . . 10 |- (b = (/) -> ~P1 b = (/))
25	24	eleq1d 2419	. . . . . . . . 9 |- (b = (/) -> (~P1 b e. n <-> (/) e. n))
26	22, 25	bi2anan9 843	. . . . . . . 8 |- ((a = (/) /\ b = (/)) -> ((~P1 a e. n /\ ~P1 b e. n) <-> ((/) e. n /\ (/) e. n)))
27	26	rexbidv 2635	. . . . . . 7 |- ((a = (/) /\ b = (/)) -> (E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> E.n e. Nn ((/) e. n /\ (/) e. n)))
28	18, 27	mpbiri 224	. . . . . 6 |- ((a = (/) /\ b = (/)) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
29	10, 11, 28	syl2anb 465	. . . . 5 |- ((a e. 0c /\ b e. 0c) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
30	29	rgen2a 2680	. . . 4 |- A.a e. 0c A.b e. 0c E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)
31		nfv 1619	. . . . . . 7 |- F/a k e. Nn
32		nfra1 2664	. . . . . . 7 |- F/aA.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)
33	31, 32	nfan 1824	. . . . . 6 |- F/a(k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
34		nfv 1619	. . . . . . . 8 |- F/b k e. Nn
35		nfra2 2668	. . . . . . . 8 |- F/bA.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)
36	34, 35	nfan 1824	. . . . . . 7 |- F/b(k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
37		nfv 1619	. . . . . . 7 |- F/b a e. (k +o 1c)
38		reeanv 2778	. . . . . . . . . 10 |- (E.c e. k E.d e. k (E.x e. ∼ ca = (c u. {x}) /\ E.y e. ∼ db = (d u. {y})) <-> (E.c e. k E.x e. ∼ ca = (c u. {x}) /\ E.d e. k E.y e. ∼ db = (d u. {y})))
39		reeanv 2778	. . . . . . . . . . 11 |- (E.x e. ∼ cE.y e. ∼ d(a = (c u. {x}) /\ b = (d u. {y})) <-> (E.x e. ∼ ca = (c u. {x}) /\ E.y e. ∼ db = (d u. {y})))
40	39	2rexbii 2641	. . . . . . . . . 10 |- (E.c e. k E.d e. k E.x e. ∼ cE.y e. ∼ d(a = (c u. {x}) /\ b = (d u. {y})) <-> E.c e. k E.d e. k (E.x e. ∼ ca = (c u. {x}) /\ E.y e. ∼ db = (d u. {y})))
41		elsuc 4413	. . . . . . . . . . 11 |- (a e. (k +o 1c) <-> E.c e. k E.x e. ∼ ca = (c u. {x}))
42		elsuc 4413	. . . . . . . . . . 11 |- (b e. (k +o 1c) <-> E.d e. k E.y e. ∼ db = (d u. {y}))
43	41, 42	anbi12i 678	. . . . . . . . . 10 |- ((a e. (k +o 1c) /\ b e. (k +o 1c)) <-> (E.c e. k E.x e. ∼ ca = (c u. {x}) /\ E.d e. k E.y e. ∼ db = (d u. {y})))
44	38, 40, 43	3bitr4ri 269	. . . . . . . . 9 |- ((a e. (k +o 1c) /\ b e. (k +o 1c)) <-> E.c e. k E.d e. k E.x e. ∼ cE.y e. ∼ d(a = (c u. {x}) /\ b = (d u. {y})))
45		pw1eq 4143	. . . . . . . . . . . . . . . . 17 |- (a = c -> ~P1 a = ~P1 c)
46	45	eleq1d 2419	. . . . . . . . . . . . . . . 16 |- (a = c -> (~P1 a e. n <-> ~P1 c e. n))
47	46	anbi1d 685	. . . . . . . . . . . . . . 15 |- (a = c -> ((~P1 a e. n /\ ~P1 b e. n) <-> (~P1 c e. n /\ ~P1 b e. n)))
48	47	rexbidv 2635	. . . . . . . . . . . . . 14 |- (a = c -> (E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> E.n e. Nn (~P1 c e. n /\ ~P1 b e. n)))
49		pw1eq 4143	. . . . . . . . . . . . . . . . 17 |- (b = d -> ~P1 b = ~P1 d)
50	49	eleq1d 2419	. . . . . . . . . . . . . . . 16 |- (b = d -> (~P1 b e. n <-> ~P1 d e. n))
51	50	anbi2d 684	. . . . . . . . . . . . . . 15 |- (b = d -> ((~P1 c e. n /\ ~P1 b e. n) <-> (~P1 c e. n /\ ~P1 d e. n)))
52	51	rexbidv 2635	. . . . . . . . . . . . . 14 |- (b = d -> (E.n e. Nn (~P1 c e. n /\ ~P1 b e. n) <-> E.n e. Nn (~P1 c e. n /\ ~P1 d e. n)))
53	48, 52	rspc2v 2961	. . . . . . . . . . . . 13 |- ((c e. k /\ d e. k) -> (A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) -> E.n e. Nn (~P1 c e. n /\ ~P1 d e. n)))
54	53	com12 27	. . . . . . . . . . . 12 |- (A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) -> ((c e. k /\ d e. k) -> E.n e. Nn (~P1 c e. n /\ ~P1 d e. n)))
55		vex 2862	. . . . . . . . . . . . . . . . . . . 20 |- x e. _V
56	55	elcompl 3225	. . . . . . . . . . . . . . . . . . 19 |- (x e. ∼ c <-> -. x e. c)
57		vex 2862	. . . . . . . . . . . . . . . . . . . 20 |- y e. _V
58	57	elcompl 3225	. . . . . . . . . . . . . . . . . . 19 |- (y e. ∼ d <-> -. y e. d)
59	56, 58	anbi12i 678	. . . . . . . . . . . . . . . . . 18 |- ((x e. ∼ c /\ y e. ∼ d) <-> (-. x e. c /\ -. y e. d))
60	59	anbi2i 675	. . . . . . . . . . . . . . . . 17 |- (((c e. k /\ d e. k) /\ (x e. ∼ c /\ y e. ∼ d)) <-> ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d)))
61		peano2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (n e. Nn -> (n +o 1c) e. Nn )
62	61	ad3antrrr 710	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> (n +o 1c) e. Nn )
63		simplrl 736	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) -> ~P1 c e. n)
64	63	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> ~P1 c e. n)
65		simprrl 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> -. x e. c)
66		snelpw1 4146	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ({x} e. ~P1 c <-> x e. c)
67	65, 66	sylnibr 296	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> -. {x} e. ~P1 c)
68		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {x} e. _V
69	68	elsuci 4414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((~P1 c e. n /\ -. {x} e. ~P1 c) -> (~P1 c u. {{x}}) e. (n +o 1c))
70	64, 67, 69	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> (~P1 c u. {{x}}) e. (n +o 1c))
71		simplrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) -> ~P1 d e. n)
72	71	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> ~P1 d e. n)
73		simprrr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> -. y e. d)
74		snelpw1 4146	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ({y} e. ~P1 d <-> y e. d)
75	73, 74	sylnibr 296	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> -. {y} e. ~P1 d)
76		snex 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {y} e. _V
77	76	elsuci 4414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((~P1 d e. n /\ -. {y} e. ~P1 d) -> (~P1 d u. {{y}}) e. (n +o 1c))
78	72, 75, 77	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> (~P1 d u. {{y}}) e. (n +o 1c))
79		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (m = (n +o 1c) -> ((~P1 c u. {{x}}) e. m <-> (~P1 c u. {{x}}) e. (n +o 1c)))
80		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (m = (n +o 1c) -> ((~P1 d u. {{y}}) e. m <-> (~P1 d u. {{y}}) e. (n +o 1c)))
81	79, 80	anbi12d 691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (m = (n +o 1c) -> (((~P1 c u. {{x}}) e. m /\ (~P1 d u. {{y}}) e. m) <-> ((~P1 c u. {{x}}) e. (n +o 1c) /\ (~P1 d u. {{y}}) e. (n +o 1c))))
82	81	rspcev 2955	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((n +o 1c) e. Nn /\ ((~P1 c u. {{x}}) e. (n +o 1c) /\ (~P1 d u. {{y}}) e. (n +o 1c))) -> E.m e. Nn ((~P1 c u. {{x}}) e. m /\ (~P1 d u. {{y}}) e. m))
83	62, 70, 78, 82	syl12anc 1180	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> E.m e. Nn ((~P1 c u. {{x}}) e. m /\ (~P1 d u. {{y}}) e. m))
84	83	ex 423	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) /\ k e. Nn ) -> (((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d)) -> E.m e. Nn ((~P1 c u. {{x}}) e. m /\ (~P1 d u. {{y}}) e. m)))
85	84	ex 423	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. Nn /\ (~P1 c e. n /\ ~P1 d e. n)) -> (k e. Nn -> (((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d)) -> E.m e. Nn ((~P1 c u. {{x}}) e. m /\ (~P1 d u. {{y}}) e. m))))
86	85	rexlimiva 2733	. . . . . . . . . . . . . . . . . . . . 21 |- (E.n e. Nn (~P1 c e. n /\ ~P1 d e. n) -> (k e. Nn -> (((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d)) -> E.m e. Nn ((~P1 c u. {{x}}) e. m /\ (~P1 d u. {{y}}) e. m))))
87		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m = n -> ((~P1 c u. {{x}}) e. m <-> (~P1 c u. {{x}}) e. n))
88		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m = n -> ((~P1 d u. {{y}}) e. m <-> (~P1 d u. {{y}}) e. n))
89	87, 88	anbi12d 691	. . . . . . . . . . . . . . . . . . . . . 22 |- (m = n -> (((~P1 c u. {{x}}) e. m /\ (~P1 d u. {{y}}) e. m) <-> ((~P1 c u. {{x}}) e. n /\ (~P1 d u. {{y}}) e. n)))
90	89	cbvrexv 2836	. . . . . . . . . . . . . . . . . . . . 21 |- (E.m e. Nn ((~P1 c u. {{x}}) e. m /\ (~P1 d u. {{y}}) e. m) <-> E.n e. Nn ((~P1 c u. {{x}}) e. n /\ (~P1 d u. {{y}}) e. n))
91	86, 90	syl8ib 222	. . . . . . . . . . . . . . . . . . . 20 |- (E.n e. Nn (~P1 c e. n /\ ~P1 d e. n) -> (k e. Nn -> (((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d)) -> E.n e. Nn ((~P1 c u. {{x}}) e. n /\ (~P1 d u. {{y}}) e. n))))
92	91	com12 27	. . . . . . . . . . . . . . . . . . 19 |- (k e. Nn -> (E.n e. Nn (~P1 c e. n /\ ~P1 d e. n) -> (((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d)) -> E.n e. Nn ((~P1 c u. {{x}}) e. n /\ (~P1 d u. {{y}}) e. n))))
93	92	imp31 421	. . . . . . . . . . . . . . . . . 18 |- (((k e. Nn /\ E.n e. Nn (~P1 c e. n /\ ~P1 d e. n)) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> E.n e. Nn ((~P1 c u. {{x}}) e. n /\ (~P1 d u. {{y}}) e. n))
94		pw1eq 4143	. . . . . . . . . . . . . . . . . . . . . 22 |- (a = (c u. {x}) -> ~P1 a = ~P1 (c u. {x}))
95		pw1un 4163	. . . . . . . . . . . . . . . . . . . . . . 23 |- ~P1 (c u. {x}) = (~P1 c u. ~P1 {x})
96	55	pw1sn 4165	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ~P1 {x} = {{x}}
97	96	uneq2i 3415	. . . . . . . . . . . . . . . . . . . . . . 23 |- (~P1 c u. ~P1 {x}) = (~P1 c u. {{x}})
98	95, 97	eqtri 2373	. . . . . . . . . . . . . . . . . . . . . 22 |- ~P1 (c u. {x}) = (~P1 c u. {{x}})
99	94, 98	syl6eq 2401	. . . . . . . . . . . . . . . . . . . . 21 |- (a = (c u. {x}) -> ~P1 a = (~P1 c u. {{x}}))
100	99	eleq1d 2419	. . . . . . . . . . . . . . . . . . . 20 |- (a = (c u. {x}) -> (~P1 a e. n <-> (~P1 c u. {{x}}) e. n))
101		pw1eq 4143	. . . . . . . . . . . . . . . . . . . . . 22 |- (b = (d u. {y}) -> ~P1 b = ~P1 (d u. {y}))
102		pw1un 4163	. . . . . . . . . . . . . . . . . . . . . . 23 |- ~P1 (d u. {y}) = (~P1 d u. ~P1 {y})
103	57	pw1sn 4165	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ~P1 {y} = {{y}}
104	103	uneq2i 3415	. . . . . . . . . . . . . . . . . . . . . . 23 |- (~P1 d u. ~P1 {y}) = (~P1 d u. {{y}})
105	102, 104	eqtri 2373	. . . . . . . . . . . . . . . . . . . . . 22 |- ~P1 (d u. {y}) = (~P1 d u. {{y}})
106	101, 105	syl6eq 2401	. . . . . . . . . . . . . . . . . . . . 21 |- (b = (d u. {y}) -> ~P1 b = (~P1 d u. {{y}}))
107	106	eleq1d 2419	. . . . . . . . . . . . . . . . . . . 20 |- (b = (d u. {y}) -> (~P1 b e. n <-> (~P1 d u. {{y}}) e. n))
108	100, 107	bi2anan9 843	. . . . . . . . . . . . . . . . . . 19 |- ((a = (c u. {x}) /\ b = (d u. {y})) -> ((~P1 a e. n /\ ~P1 b e. n) <-> ((~P1 c u. {{x}}) e. n /\ (~P1 d u. {{y}}) e. n)))
109	108	rexbidv 2635	. . . . . . . . . . . . . . . . . 18 |- ((a = (c u. {x}) /\ b = (d u. {y})) -> (E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> E.n e. Nn ((~P1 c u. {{x}}) e. n /\ (~P1 d u. {{y}}) e. n)))
110	93, 109	syl5ibrcom 213	. . . . . . . . . . . . . . . . 17 |- (((k e. Nn /\ E.n e. Nn (~P1 c e. n /\ ~P1 d e. n)) /\ ((c e. k /\ d e. k) /\ (-. x e. c /\ -. y e. d))) -> ((a = (c u. {x}) /\ b = (d u. {y})) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
111	60, 110	sylan2b 461	. . . . . . . . . . . . . . . 16 |- (((k e. Nn /\ E.n e. Nn (~P1 c e. n /\ ~P1 d e. n)) /\ ((c e. k /\ d e. k) /\ (x e. ∼ c /\ y e. ∼ d))) -> ((a = (c u. {x}) /\ b = (d u. {y})) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
112	111	expr 598	. . . . . . . . . . . . . . 15 |- (((k e. Nn /\ E.n e. Nn (~P1 c e. n /\ ~P1 d e. n)) /\ (c e. k /\ d e. k)) -> ((x e. ∼ c /\ y e. ∼ d) -> ((a = (c u. {x}) /\ b = (d u. {y})) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))))
113	112	anasss 628	. . . . . . . . . . . . . 14 |- ((k e. Nn /\ (E.n e. Nn (~P1 c e. n /\ ~P1 d e. n) /\ (c e. k /\ d e. k))) -> ((x e. ∼ c /\ y e. ∼ d) -> ((a = (c u. {x}) /\ b = (d u. {y})) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))))
114	113	rexlimdvv 2744	. . . . . . . . . . . . 13 |- ((k e. Nn /\ (E.n e. Nn (~P1 c e. n /\ ~P1 d e. n) /\ (c e. k /\ d e. k))) -> (E.x e. ∼ cE.y e. ∼ d(a = (c u. {x}) /\ b = (d u. {y})) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
115	114	exp32 588	. . . . . . . . . . . 12 |- (k e. Nn -> (E.n e. Nn (~P1 c e. n /\ ~P1 d e. n) -> ((c e. k /\ d e. k) -> (E.x e. ∼ cE.y e. ∼ d(a = (c u. {x}) /\ b = (d u. {y})) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))))
116	54, 115	sylan9r 639	. . . . . . . . . . 11 |- ((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)) -> ((c e. k /\ d e. k) -> ((c e. k /\ d e. k) -> (E.x e. ∼ cE.y e. ∼ d(a = (c u. {x}) /\ b = (d u. {y})) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))))
117	116	pm2.43d 44	. . . . . . . . . 10 |- ((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)) -> ((c e. k /\ d e. k) -> (E.x e. ∼ cE.y e. ∼ d(a = (c u. {x}) /\ b = (d u. {y})) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))))
118	117	rexlimdvv 2744	. . . . . . . . 9 |- ((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)) -> (E.c e. k E.d e. k E.x e. ∼ cE.y e. ∼ d(a = (c u. {x}) /\ b = (d u. {y})) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
119	44, 118	syl5bi 208	. . . . . . . 8 |- ((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)) -> ((a e. (k +o 1c) /\ b e. (k +o 1c)) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
120	119	exp3a 425	. . . . . . 7 |- ((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)) -> (a e. (k +o 1c) -> (b e. (k +o 1c) -> E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))))
121	36, 37, 120	ralrimd 2702	. . . . . 6 |- ((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)) -> (a e. (k +o 1c) -> A.b e. (k +o 1c)E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
122	33, 121	ralrimi 2695	. . . . 5 |- ((k e. Nn /\ A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)) -> A.a e. (k +o 1c)A.b e. (k +o 1c)E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
123	122	ex 423	. . . 4 |- (k e. Nn -> (A.a e. k A.b e. k E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) -> A.a e. (k +o 1c)A.b e. (k +o 1c)E.n e. Nn (~P1 a e. n /\ ~P1 b e. n)))
124	1, 3, 5, 7, 9, 30, 123	finds 4411	. . 3 |- (M e. Nn -> A.a e. M A.b e. M E.n e. Nn (~P1 a e. n /\ ~P1 b e. n))
125		pw1eq 4143	. . . . . . 7 |- (a = A -> ~P1 a = ~P1 A)
126	125	eleq1d 2419	. . . . . 6 |- (a = A -> (~P1 a e. n <-> ~P1 A e. n))
127	126	anbi1d 685	. . . . 5 |- (a = A -> ((~P1 a e. n /\ ~P1 b e. n) <-> (~P1 A e. n /\ ~P1 b e. n)))
128	127	rexbidv 2635	. . . 4 |- (a = A -> (E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) <-> E.n e. Nn (~P1 A e. n /\ ~P1 b e. n)))
129		pw1eq 4143	. . . . . . 7 |- (b = B -> ~P1 b = ~P1 B)
130	129	eleq1d 2419	. . . . . 6 |- (b = B -> (~P1 b e. n <-> ~P1 B e. n))
131	130	anbi2d 684	. . . . 5 |- (b = B -> ((~P1 A e. n /\ ~P1 b e. n) <-> (~P1 A e. n /\ ~P1 B e. n)))
132	131	rexbidv 2635	. . . 4 |- (b = B -> (E.n e. Nn (~P1 A e. n /\ ~P1 b e. n) <-> E.n e. Nn (~P1 A e. n /\ ~P1 B e. n)))
133	128, 132	rspc2v 2961	. . 3 |- ((A e. M /\ B e. M) -> (A.a e. M A.b e. M E.n e. Nn (~P1 a e. n /\ ~P1 b e. n) -> E.n e. Nn (~P1 A e. n /\ ~P1 B e. n)))
134	124, 133	syl5com 26	. 2 |- (M e. Nn -> ((A e. M /\ B e. M) -> E.n e. Nn (~P1 A e. n /\ ~P1 B e. n)))
135	134	3impib 1149	1 |- ((M e. Nn /\ A e. M /\ B e. M) -> E.n e. Nn (~P1 A e. n /\ ~P1 B e. n))

Syntax hints:  -. wn 3   -> wi 4   /\ wa 358   /\ w3a 934   = wceq 1642   e. wcel 1710  A.wral 2614  E.wrex 2615   ∼ ccompl 3205   u. cun 3207  (/)c0 3550  {csn 3737  1_cc1c 4134  ~P₁ cpw1 4135   Nn cnnc 4373  0_cc0c 4374   +o cplc 4375

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-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087

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 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-0c 4377  df-addc 4378  df-nnc 4379

This theorem is referenced by:  nnpw1ex  4484  tfinpw1  4494  pw1fin  6169