Theorem ncfinlower 4484

Description: If the unit power classes of two sets are in the same natural, then so are the sets themselves. Theorem X.1.26 of [Rosser] p. 527. (Contributed by SF, 22-Jan-2015.)

Assertion

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

Distinct variable groups:   A,n   B,n

Allowed substitution hint:   M(n)

Proof of Theorem ncfinlower

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

Step	Hyp	Ref	Expression
1		ncfinlowerlem1 4483	. . . 4 |- {m | A.aA.b((~P1 a e. m /\ ~P1 b e. m) -> E.n e. Nn (a e. n /\ b e. n))} e. _V
2		eleq2 2414	. . . . . . 7 |- (m = 0c -> (~P1 a e. m <-> ~P1 a e. 0c))
3		eleq2 2414	. . . . . . 7 |- (m = 0c -> (~P1 b e. m <-> ~P1 b e. 0c))
4	2, 3	anbi12d 691	. . . . . 6 |- (m = 0c -> ((~P1 a e. m /\ ~P1 b e. m) <-> (~P1 a e. 0c /\ ~P1 b e. 0c)))
5	4	imbi1d 308	. . . . 5 |- (m = 0c -> (((~P1 a e. m /\ ~P1 b e. m) -> E.n e. Nn (a e. n /\ b e. n)) <-> ((~P1 a e. 0c /\ ~P1 b e. 0c) -> E.n e. Nn (a e. n /\ b e. n))))
6	5	2albidv 1627	. . . 4 |- (m = 0c -> (A.aA.b((~P1 a e. m /\ ~P1 b e. m) -> E.n e. Nn (a e. n /\ b e. n)) <-> A.aA.b((~P1 a e. 0c /\ ~P1 b e. 0c) -> E.n e. Nn (a e. n /\ b e. n))))
7		eleq2 2414	. . . . . . 7 |- (m = k -> (~P1 a e. m <-> ~P1 a e. k))
8		eleq2 2414	. . . . . . 7 |- (m = k -> (~P1 b e. m <-> ~P1 b e. k))
9	7, 8	anbi12d 691	. . . . . 6 |- (m = k -> ((~P1 a e. m /\ ~P1 b e. m) <-> (~P1 a e. k /\ ~P1 b e. k)))
10	9	imbi1d 308	. . . . 5 |- (m = k -> (((~P1 a e. m /\ ~P1 b e. m) -> E.n e. Nn (a e. n /\ b e. n)) <-> ((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))))
11	10	2albidv 1627	. . . 4 |- (m = k -> (A.aA.b((~P1 a e. m /\ ~P1 b e. m) -> E.n e. Nn (a e. n /\ b e. n)) <-> A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))))
12		eleq2 2414	. . . . . . 7 |- (m = (k +o 1c) -> (~P1 a e. m <-> ~P1 a e. (k +o 1c)))
13		eleq2 2414	. . . . . . 7 |- (m = (k +o 1c) -> (~P1 b e. m <-> ~P1 b e. (k +o 1c)))
14	12, 13	anbi12d 691	. . . . . 6 |- (m = (k +o 1c) -> ((~P1 a e. m /\ ~P1 b e. m) <-> (~P1 a e. (k +o 1c) /\ ~P1 b e. (k +o 1c))))
15	14	imbi1d 308	. . . . 5 |- (m = (k +o 1c) -> (((~P1 a e. m /\ ~P1 b e. m) -> E.n e. Nn (a e. n /\ b e. n)) <-> ((~P1 a e. (k +o 1c) /\ ~P1 b e. (k +o 1c)) -> E.n e. Nn (a e. n /\ b e. n))))
16	15	2albidv 1627	. . . 4 |- (m = (k +o 1c) -> (A.aA.b((~P1 a e. m /\ ~P1 b e. m) -> E.n e. Nn (a e. n /\ b e. n)) <-> A.aA.b((~P1 a e. (k +o 1c) /\ ~P1 b e. (k +o 1c)) -> E.n e. Nn (a e. n /\ b e. n))))
17		eleq2 2414	. . . . . . 7 |- (m = M -> (~P1 a e. m <-> ~P1 a e. M))
18		eleq2 2414	. . . . . . 7 |- (m = M -> (~P1 b e. m <-> ~P1 b e. M))
19	17, 18	anbi12d 691	. . . . . 6 |- (m = M -> ((~P1 a e. m /\ ~P1 b e. m) <-> (~P1 a e. M /\ ~P1 b e. M)))
20	19	imbi1d 308	. . . . 5 |- (m = M -> (((~P1 a e. m /\ ~P1 b e. m) -> E.n e. Nn (a e. n /\ b e. n)) <-> ((~P1 a e. M /\ ~P1 b e. M) -> E.n e. Nn (a e. n /\ b e. n))))
21	20	2albidv 1627	. . . 4 |- (m = M -> (A.aA.b((~P1 a e. m /\ ~P1 b e. m) -> E.n e. Nn (a e. n /\ b e. n)) <-> A.aA.b((~P1 a e. M /\ ~P1 b e. M) -> E.n e. Nn (a e. n /\ b e. n))))
22		el0c 4422	. . . . . . 7 |- (~P1 a e. 0c <-> ~P1 a = (/))
23		pw10b 4167	. . . . . . 7 |- (~P1 a = (/) <-> a = (/))
24	22, 23	bitri 240	. . . . . 6 |- (~P1 a e. 0c <-> a = (/))
25		el0c 4422	. . . . . . 7 |- (~P1 b e. 0c <-> ~P1 b = (/))
26		pw10b 4167	. . . . . . 7 |- (~P1 b = (/) <-> b = (/))
27	25, 26	bitri 240	. . . . . 6 |- (~P1 b e. 0c <-> b = (/))
28		peano1 4403	. . . . . . . 8 |- 0c e. Nn
29		nulel0c 4423	. . . . . . . 8 |- (/) e. 0c
30		eleq2 2414	. . . . . . . . 9 |- (n = 0c -> ((/) e. n <-> (/) e. 0c))
31	30	rspcev 2956	. . . . . . . 8 |- ((0c e. Nn /\ (/) e. 0c) -> E.n e. Nn (/) e. n)
32	28, 29, 31	mp2an 653	. . . . . . 7 |- E.n e. Nn (/) e. n
33		eleq1 2413	. . . . . . . . . 10 |- (a = (/) -> (a e. n <-> (/) e. n))
34		eleq1 2413	. . . . . . . . . 10 |- (b = (/) -> (b e. n <-> (/) e. n))
35	33, 34	bi2anan9 843	. . . . . . . . 9 |- ((a = (/) /\ b = (/)) -> ((a e. n /\ b e. n) <-> ((/) e. n /\ (/) e. n)))
36		anidm 625	. . . . . . . . 9 |- (((/) e. n /\ (/) e. n) <-> (/) e. n)
37	35, 36	syl6bb 252	. . . . . . . 8 |- ((a = (/) /\ b = (/)) -> ((a e. n /\ b e. n) <-> (/) e. n))
38	37	rexbidv 2636	. . . . . . 7 |- ((a = (/) /\ b = (/)) -> (E.n e. Nn (a e. n /\ b e. n) <-> E.n e. Nn (/) e. n))
39	32, 38	mpbiri 224	. . . . . 6 |- ((a = (/) /\ b = (/)) -> E.n e. Nn (a e. n /\ b e. n))
40	24, 27, 39	syl2anb 465	. . . . 5 |- ((~P1 a e. 0c /\ ~P1 b e. 0c) -> E.n e. Nn (a e. n /\ b e. n))
41	40	gen2 1547	. . . 4 |- A.aA.b((~P1 a e. 0c /\ ~P1 b e. 0c) -> E.n e. Nn (a e. n /\ b e. n))
42		nfv 1619	. . . . . . 7 |- F/a k e. Nn
43		nfa1 1788	. . . . . . 7 |- F/aA.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))
44	42, 43	nfan 1824	. . . . . 6 |- F/a(k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n)))
45		nfv 1619	. . . . . . . 8 |- F/b k e. Nn
46		nfa2 1855	. . . . . . . 8 |- F/bA.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))
47	45, 46	nfan 1824	. . . . . . 7 |- F/b(k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n)))
48		reeanv 2779	. . . . . . . . 9 |- (E.c e. k E.d e. k (E.x e. ∼ c~P1 a = (c u. {x}) /\ E.y e. ∼ d~P1 b = (d u. {y})) <-> (E.c e. k E.x e. ∼ c~P1 a = (c u. {x}) /\ E.d e. k E.y e. ∼ d~P1 b = (d u. {y})))
49		reeanv 2779	. . . . . . . . . 10 |- (E.x e. ∼ cE.y e. ∼ d(~P1 a = (c u. {x}) /\ ~P1 b = (d u. {y})) <-> (E.x e. ∼ c~P1 a = (c u. {x}) /\ E.y e. ∼ d~P1 b = (d u. {y})))
50	49	2rexbii 2642	. . . . . . . . 9 |- (E.c e. k E.d e. k E.x e. ∼ cE.y e. ∼ d(~P1 a = (c u. {x}) /\ ~P1 b = (d u. {y})) <-> E.c e. k E.d e. k (E.x e. ∼ c~P1 a = (c u. {x}) /\ E.y e. ∼ d~P1 b = (d u. {y})))
51		elsuc 4414	. . . . . . . . . 10 |- (~P1 a e. (k +o 1c) <-> E.c e. k E.x e. ∼ c~P1 a = (c u. {x}))
52		elsuc 4414	. . . . . . . . . 10 |- (~P1 b e. (k +o 1c) <-> E.d e. k E.y e. ∼ d~P1 b = (d u. {y}))
53	51, 52	anbi12i 678	. . . . . . . . 9 |- ((~P1 a e. (k +o 1c) /\ ~P1 b e. (k +o 1c)) <-> (E.c e. k E.x e. ∼ c~P1 a = (c u. {x}) /\ E.d e. k E.y e. ∼ d~P1 b = (d u. {y})))
54	48, 50, 53	3bitr4ri 269	. . . . . . . 8 |- ((~P1 a e. (k +o 1c) /\ ~P1 b e. (k +o 1c)) <-> E.c e. k E.d e. k E.x e. ∼ cE.y e. ∼ d(~P1 a = (c u. {x}) /\ ~P1 b = (d u. {y})))
55		vex 2863	. . . . . . . . . . . . . . . . . . . . . 22 |- e e. _V
56		vex 2863	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
57		pw1eq 4144	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (a = e -> ~P1 a = ~P1 e)
58	57	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (a = e -> (~P1 a e. k <-> ~P1 e e. k))
59		pw1eq 4144	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (b = f -> ~P1 b = ~P1 f)
60	59	eleq1d 2419	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (b = f -> (~P1 b e. k <-> ~P1 f e. k))
61	58, 60	bi2anan9 843	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a = e /\ b = f) -> ((~P1 a e. k /\ ~P1 b e. k) <-> (~P1 e e. k /\ ~P1 f e. k)))
62		elequ1 1713	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (a = e -> (a e. n <-> e e. n))
63		elequ1 1713	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (b = f -> (b e. n <-> f e. n))
64	62, 63	bi2anan9 843	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((a = e /\ b = f) -> ((a e. n /\ b e. n) <-> (e e. n /\ f e. n)))
65	64	rexbidv 2636	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a = e /\ b = f) -> (E.n e. Nn (a e. n /\ b e. n) <-> E.n e. Nn (e e. n /\ f e. n)))
66	61, 65	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((a = e /\ b = f) -> (((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n)) <-> ((~P1 e e. k /\ ~P1 f e. k) -> E.n e. Nn (e e. n /\ f e. n))))
67	66	spc2gv 2943	. . . . . . . . . . . . . . . . . . . . . 22 |- ((e e. _V /\ f e. _V) -> (A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n)) -> ((~P1 e e. k /\ ~P1 f e. k) -> E.n e. Nn (e e. n /\ f e. n))))
68	55, 56, 67	mp2an 653	. . . . . . . . . . . . . . . . . . . . 21 |- (A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n)) -> ((~P1 e e. k /\ ~P1 f e. k) -> E.n e. Nn (e e. n /\ f e. n)))
69	68	com12 27	. . . . . . . . . . . . . . . . . . . 20 |- ((~P1 e e. k /\ ~P1 f e. k) -> (A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n)) -> E.n e. Nn (e e. n /\ f e. n)))
70	69	ad2antrl 708	. . . . . . . . . . . . . . . . . . 19 |- ((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) -> (A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n)) -> E.n e. Nn (e e. n /\ f e. n)))
71		peano2 4404	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n e. Nn -> (n +o 1c) e. Nn )
72	71	ad2antrl 708	. . . . . . . . . . . . . . . . . . . . . 22 |- (((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) /\ (n e. Nn /\ (e e. n /\ f e. n))) -> (n +o 1c) e. Nn )
73		simprrl 740	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) /\ (n e. Nn /\ (e e. n /\ f e. n))) -> e e. n)
74		simprrl 740	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) -> -. z e. e)
75	74	adantr 451	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) /\ (n e. Nn /\ (e e. n /\ f e. n))) -> -. z e. e)
76		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . 24 |- z e. _V
77	76	elsuci 4415	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((e e. n /\ -. z e. e) -> (e u. {z}) e. (n +o 1c))
78	73, 75, 77	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . 22 |- (((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) /\ (n e. Nn /\ (e e. n /\ f e. n))) -> (e u. {z}) e. (n +o 1c))
79		simprrr 741	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) /\ (n e. Nn /\ (e e. n /\ f e. n))) -> f e. n)
80		simprrr 741	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) -> -. w e. f)
81	80	adantr 451	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) /\ (n e. Nn /\ (e e. n /\ f e. n))) -> -. w e. f)
82		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . 24 |- w e. _V
83	82	elsuci 4415	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f e. n /\ -. w e. f) -> (f u. {w}) e. (n +o 1c))
84	79, 81, 83	syl2anc 642	. . . . . . . . . . . . . . . . . . . . . 22 |- (((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) /\ (n e. Nn /\ (e e. n /\ f e. n))) -> (f u. {w}) e. (n +o 1c))
85		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (m = (n +o 1c) -> ((e u. {z}) e. m <-> (e u. {z}) e. (n +o 1c)))
86		eleq2 2414	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (m = (n +o 1c) -> ((f u. {w}) e. m <-> (f u. {w}) e. (n +o 1c)))
87	85, 86	anbi12d 691	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m = (n +o 1c) -> (((e u. {z}) e. m /\ (f u. {w}) e. m) <-> ((e u. {z}) e. (n +o 1c) /\ (f u. {w}) e. (n +o 1c))))
88	87	rspcev 2956	. . . . . . . . . . . . . . . . . . . . . 22 |- (((n +o 1c) e. Nn /\ ((e u. {z}) e. (n +o 1c) /\ (f u. {w}) e. (n +o 1c))) -> E.m e. Nn ((e u. {z}) e. m /\ (f u. {w}) e. m))
89	72, 78, 84, 88	syl12anc 1180	. . . . . . . . . . . . . . . . . . . . 21 |- (((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) /\ (n e. Nn /\ (e e. n /\ f e. n))) -> E.m e. Nn ((e u. {z}) e. m /\ (f u. {w}) e. m))
90	89	expr 598	. . . . . . . . . . . . . . . . . . . 20 |- (((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) /\ n e. Nn ) -> ((e e. n /\ f e. n) -> E.m e. Nn ((e u. {z}) e. m /\ (f u. {w}) e. m)))
91	90	rexlimdva 2739	. . . . . . . . . . . . . . . . . . 19 |- ((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) -> (E.n e. Nn (e e. n /\ f e. n) -> E.m e. Nn ((e u. {z}) e. m /\ (f u. {w}) e. m)))
92	70, 91	syld 40	. . . . . . . . . . . . . . . . . 18 |- ((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) -> (A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n)) -> E.m e. Nn ((e u. {z}) e. m /\ (f u. {w}) e. m)))
93	92	imp 418	. . . . . . . . . . . . . . . . 17 |- (((k e. Nn /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) -> E.m e. Nn ((e u. {z}) e. m /\ (f u. {w}) e. m))
94	93	an32s 779	. . . . . . . . . . . . . . . 16 |- (((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) -> E.m e. Nn ((e u. {z}) e. m /\ (f u. {w}) e. m))
95		eleq1 2413	. . . . . . . . . . . . . . . . . . . . 21 |- (c = ~P1 e -> (c e. k <-> ~P1 e e. k))
96	95	3ad2ant2 977	. . . . . . . . . . . . . . . . . . . 20 |- ((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) -> (c e. k <-> ~P1 e e. k))
97		eleq1 2413	. . . . . . . . . . . . . . . . . . . . 21 |- (d = ~P1 f -> (d e. k <-> ~P1 f e. k))
98	97	3ad2ant2 977	. . . . . . . . . . . . . . . . . . . 20 |- ((b = (f u. {w}) /\ d = ~P1 f /\ y = {w}) -> (d e. k <-> ~P1 f e. k))
99	96, 98	bi2anan9 843	. . . . . . . . . . . . . . . . . . 19 |- (((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> ((c e. k /\ d e. k) <-> (~P1 e e. k /\ ~P1 f e. k)))
100		compleq 3244	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (c = ~P1 e -> ∼ c = ∼ ~P1 e)
101		eleq12 2415	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x = {z} /\ ∼ c = ∼ ~P1 e) -> (x e. ∼ c <-> {z} e. ∼ ~P1 e))
102	100, 101	sylan2 460	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x = {z} /\ c = ~P1 e) -> (x e. ∼ c <-> {z} e. ∼ ~P1 e))
103		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- {z} e. _V
104	103	elcompl 3226	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ({z} e. ∼ ~P1 e <-> -. {z} e. ~P1 e)
105		snelpw1 4147	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ({z} e. ~P1 e <-> z e. e)
106	104, 105	xchbinx 301	. . . . . . . . . . . . . . . . . . . . . . 23 |- ({z} e. ∼ ~P1 e <-> -. z e. e)
107	102, 106	syl6bb 252	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x = {z} /\ c = ~P1 e) -> (x e. ∼ c <-> -. z e. e))
108	107	ancoms 439	. . . . . . . . . . . . . . . . . . . . 21 |- ((c = ~P1 e /\ x = {z}) -> (x e. ∼ c <-> -. z e. e))
109	108	3adant1 973	. . . . . . . . . . . . . . . . . . . 20 |- ((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) -> (x e. ∼ c <-> -. z e. e))
110		compleq 3244	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (d = ~P1 f -> ∼ d = ∼ ~P1 f)
111		eleq12 2415	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y = {w} /\ ∼ d = ∼ ~P1 f) -> (y e. ∼ d <-> {w} e. ∼ ~P1 f))
112	110, 111	sylan2 460	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y = {w} /\ d = ~P1 f) -> (y e. ∼ d <-> {w} e. ∼ ~P1 f))
113		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- {w} e. _V
114	113	elcompl 3226	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ({w} e. ∼ ~P1 f <-> -. {w} e. ~P1 f)
115		snelpw1 4147	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ({w} e. ~P1 f <-> w e. f)
116	114, 115	xchbinx 301	. . . . . . . . . . . . . . . . . . . . . . 23 |- ({w} e. ∼ ~P1 f <-> -. w e. f)
117	112, 116	syl6bb 252	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y = {w} /\ d = ~P1 f) -> (y e. ∼ d <-> -. w e. f))
118	117	ancoms 439	. . . . . . . . . . . . . . . . . . . . 21 |- ((d = ~P1 f /\ y = {w}) -> (y e. ∼ d <-> -. w e. f))
119	118	3adant1 973	. . . . . . . . . . . . . . . . . . . 20 |- ((b = (f u. {w}) /\ d = ~P1 f /\ y = {w}) -> (y e. ∼ d <-> -. w e. f))
120	109, 119	bi2anan9 843	. . . . . . . . . . . . . . . . . . 19 |- (((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> ((x e. ∼ c /\ y e. ∼ d) <-> (-. z e. e /\ -. w e. f)))
121	99, 120	anbi12d 691	. . . . . . . . . . . . . . . . . 18 |- (((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> (((c e. k /\ d e. k) /\ (x e. ∼ c /\ y e. ∼ d)) <-> ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))))
122	121	anbi2d 684	. . . . . . . . . . . . . . . . 17 |- (((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> (((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ ((c e. k /\ d e. k) /\ (x e. ∼ c /\ y e. ∼ d))) <-> ((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f)))))
123		eleq1 2413	. . . . . . . . . . . . . . . . . . . 20 |- (a = (e u. {z}) -> (a e. m <-> (e u. {z}) e. m))
124	123	3ad2ant1 976	. . . . . . . . . . . . . . . . . . 19 |- ((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) -> (a e. m <-> (e u. {z}) e. m))
125		eleq1 2413	. . . . . . . . . . . . . . . . . . . 20 |- (b = (f u. {w}) -> (b e. m <-> (f u. {w}) e. m))
126	125	3ad2ant1 976	. . . . . . . . . . . . . . . . . . 19 |- ((b = (f u. {w}) /\ d = ~P1 f /\ y = {w}) -> (b e. m <-> (f u. {w}) e. m))
127	124, 126	bi2anan9 843	. . . . . . . . . . . . . . . . . 18 |- (((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> ((a e. m /\ b e. m) <-> ((e u. {z}) e. m /\ (f u. {w}) e. m)))
128	127	rexbidv 2636	. . . . . . . . . . . . . . . . 17 |- (((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> (E.m e. Nn (a e. m /\ b e. m) <-> E.m e. Nn ((e u. {z}) e. m /\ (f u. {w}) e. m)))
129	122, 128	imbi12d 311	. . . . . . . . . . . . . . . 16 |- (((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> ((((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ ((c e. k /\ d e. k) /\ (x e. ∼ c /\ y e. ∼ d))) -> E.m e. Nn (a e. m /\ b e. m)) <-> (((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ ((~P1 e e. k /\ ~P1 f e. k) /\ (-. z e. e /\ -. w e. f))) -> E.m e. Nn ((e u. {z}) e. m /\ (f u. {w}) e. m))))
130	94, 129	mpbiri 224	. . . . . . . . . . . . . . 15 |- (((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> (((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ ((c e. k /\ d e. k) /\ (x e. ∼ c /\ y e. ∼ d))) -> E.m e. Nn (a e. m /\ b e. m)))
131	130	com12 27	. . . . . . . . . . . . . 14 |- (((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ ((c e. k /\ d e. k) /\ (x e. ∼ c /\ y e. ∼ d))) -> (((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> E.m e. Nn (a e. m /\ b e. m)))
132	131	exlimdvv 1637	. . . . . . . . . . . . 13 |- (((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ ((c e. k /\ d e. k) /\ (x e. ∼ c /\ y e. ∼ d))) -> (E.zE.w((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> E.m e. Nn (a e. m /\ b e. m)))
133	132	exlimdvv 1637	. . . . . . . . . . . 12 |- (((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ ((c e. k /\ d e. k) /\ (x e. ∼ c /\ y e. ∼ d))) -> (E.eE.fE.zE.w((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) -> E.m e. Nn (a e. m /\ b e. m)))
134		eeanv 1913	. . . . . . . . . . . . 13 |- (E.eE.f(E.z(a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ E.w(b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) <-> (E.eE.z(a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ E.fE.w(b = (f u. {w}) /\ d = ~P1 f /\ y = {w})))
135		eeanv 1913	. . . . . . . . . . . . . 14 |- (E.zE.w((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) <-> (E.z(a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ E.w(b = (f u. {w}) /\ d = ~P1 f /\ y = {w})))
136	135	2exbii 1583	. . . . . . . . . . . . 13 |- (E.eE.fE.zE.w((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})) <-> E.eE.f(E.z(a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ E.w(b = (f u. {w}) /\ d = ~P1 f /\ y = {w})))
137		vex 2863	. . . . . . . . . . . . . . 15 |- c e. _V
138		vex 2863	. . . . . . . . . . . . . . 15 |- x e. _V
139	137, 138	pw1eqadj 4333	. . . . . . . . . . . . . 14 |- (~P1 a = (c u. {x}) <-> E.eE.z(a = (e u. {z}) /\ c = ~P1 e /\ x = {z}))
140		vex 2863	. . . . . . . . . . . . . . 15 |- d e. _V
141		vex 2863	. . . . . . . . . . . . . . 15 |- y e. _V
142	140, 141	pw1eqadj 4333	. . . . . . . . . . . . . 14 |- (~P1 b = (d u. {y}) <-> E.fE.w(b = (f u. {w}) /\ d = ~P1 f /\ y = {w}))
143	139, 142	anbi12i 678	. . . . . . . . . . . . 13 |- ((~P1 a = (c u. {x}) /\ ~P1 b = (d u. {y})) <-> (E.eE.z(a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ E.fE.w(b = (f u. {w}) /\ d = ~P1 f /\ y = {w})))
144	134, 136, 143	3bitr4ri 269	. . . . . . . . . . . 12 |- ((~P1 a = (c u. {x}) /\ ~P1 b = (d u. {y})) <-> E.eE.fE.zE.w((a = (e u. {z}) /\ c = ~P1 e /\ x = {z}) /\ (b = (f u. {w}) /\ d = ~P1 f /\ y = {w})))
145		elequ2 1715	. . . . . . . . . . . . . 14 |- (n = m -> (a e. n <-> a e. m))
146		elequ2 1715	. . . . . . . . . . . . . 14 |- (n = m -> (b e. n <-> b e. m))
147	145, 146	anbi12d 691	. . . . . . . . . . . . 13 |- (n = m -> ((a e. n /\ b e. n) <-> (a e. m /\ b e. m)))
148	147	cbvrexv 2837	. . . . . . . . . . . 12 |- (E.n e. Nn (a e. n /\ b e. n) <-> E.m e. Nn (a e. m /\ b e. m))
149	133, 144, 148	3imtr4g 261	. . . . . . . . . . 11 |- (((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ ((c e. k /\ d e. k) /\ (x e. ∼ c /\ y e. ∼ d))) -> ((~P1 a = (c u. {x}) /\ ~P1 b = (d u. {y})) -> E.n e. Nn (a e. n /\ b e. n)))
150	149	expr 598	. . . . . . . . . 10 |- (((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ (c e. k /\ d e. k)) -> ((x e. ∼ c /\ y e. ∼ d) -> ((~P1 a = (c u. {x}) /\ ~P1 b = (d u. {y})) -> E.n e. Nn (a e. n /\ b e. n))))
151	150	rexlimdvv 2745	. . . . . . . . 9 |- (((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) /\ (c e. k /\ d e. k)) -> (E.x e. ∼ cE.y e. ∼ d(~P1 a = (c u. {x}) /\ ~P1 b = (d u. {y})) -> E.n e. Nn (a e. n /\ b e. n)))
152	151	rexlimdvva 2746	. . . . . . . 8 |- ((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) -> (E.c e. k E.d e. k E.x e. ∼ cE.y e. ∼ d(~P1 a = (c u. {x}) /\ ~P1 b = (d u. {y})) -> E.n e. Nn (a e. n /\ b e. n)))
153	54, 152	syl5bi 208	. . . . . . 7 |- ((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) -> ((~P1 a e. (k +o 1c) /\ ~P1 b e. (k +o 1c)) -> E.n e. Nn (a e. n /\ b e. n)))
154	47, 153	alrimi 1765	. . . . . 6 |- ((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) -> A.b((~P1 a e. (k +o 1c) /\ ~P1 b e. (k +o 1c)) -> E.n e. Nn (a e. n /\ b e. n)))
155	44, 154	alrimi 1765	. . . . 5 |- ((k e. Nn /\ A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n))) -> A.aA.b((~P1 a e. (k +o 1c) /\ ~P1 b e. (k +o 1c)) -> E.n e. Nn (a e. n /\ b e. n)))
156	155	ex 423	. . . 4 |- (k e. Nn -> (A.aA.b((~P1 a e. k /\ ~P1 b e. k) -> E.n e. Nn (a e. n /\ b e. n)) -> A.aA.b((~P1 a e. (k +o 1c) /\ ~P1 b e. (k +o 1c)) -> E.n e. Nn (a e. n /\ b e. n))))
157	1, 6, 11, 16, 21, 41, 156	finds 4412	. . 3 |- (M e. Nn -> A.aA.b((~P1 a e. M /\ ~P1 b e. M) -> E.n e. Nn (a e. n /\ b e. n)))
158		elex 2868	. . . . . 6 |- (~P1 A e. M -> ~P1 A e. _V)
159		pw1exb 4327	. . . . . 6 |- (~P1 A e. _V <-> A e. _V)
160	158, 159	sylib 188	. . . . 5 |- (~P1 A e. M -> A e. _V)
161		elex 2868	. . . . . 6 |- (~P1 B e. M -> ~P1 B e. _V)
162		pw1exb 4327	. . . . . 6 |- (~P1 B e. _V <-> B e. _V)
163	161, 162	sylib 188	. . . . 5 |- (~P1 B e. M -> B e. _V)
164		pw1eq 4144	. . . . . . . . 9 |- (a = A -> ~P1 a = ~P1 A)
165	164	eleq1d 2419	. . . . . . . 8 |- (a = A -> (~P1 a e. M <-> ~P1 A e. M))
166		pw1eq 4144	. . . . . . . . 9 |- (b = B -> ~P1 b = ~P1 B)
167	166	eleq1d 2419	. . . . . . . 8 |- (b = B -> (~P1 b e. M <-> ~P1 B e. M))
168	165, 167	bi2anan9 843	. . . . . . 7 |- ((a = A /\ b = B) -> ((~P1 a e. M /\ ~P1 b e. M) <-> (~P1 A e. M /\ ~P1 B e. M)))
169		eleq1 2413	. . . . . . . . 9 |- (a = A -> (a e. n <-> A e. n))
170		eleq1 2413	. . . . . . . . 9 |- (b = B -> (b e. n <-> B e. n))
171	169, 170	bi2anan9 843	. . . . . . . 8 |- ((a = A /\ b = B) -> ((a e. n /\ b e. n) <-> (A e. n /\ B e. n)))
172	171	rexbidv 2636	. . . . . . 7 |- ((a = A /\ b = B) -> (E.n e. Nn (a e. n /\ b e. n) <-> E.n e. Nn (A e. n /\ B e. n)))
173	168, 172	imbi12d 311	. . . . . 6 |- ((a = A /\ b = B) -> (((~P1 a e. M /\ ~P1 b e. M) -> E.n e. Nn (a e. n /\ b e. n)) <-> ((~P1 A e. M /\ ~P1 B e. M) -> E.n e. Nn (A e. n /\ B e. n))))
174	173	spc2gv 2943	. . . . 5 |- ((A e. _V /\ B e. _V) -> (A.aA.b((~P1 a e. M /\ ~P1 b e. M) -> E.n e. Nn (a e. n /\ b e. n)) -> ((~P1 A e. M /\ ~P1 B e. M) -> E.n e. Nn (A e. n /\ B e. n))))
175	160, 163, 174	syl2an 463	. . . 4 |- ((~P1 A e. M /\ ~P1 B e. M) -> (A.aA.b((~P1 a e. M /\ ~P1 b e. M) -> E.n e. Nn (a e. n /\ b e. n)) -> ((~P1 A e. M /\ ~P1 B e. M) -> E.n e. Nn (A e. n /\ B e. n))))
176	175	pm2.43b 46	. . 3 |- (A.aA.b((~P1 a e. M /\ ~P1 b e. M) -> E.n e. Nn (a e. n /\ b e. n)) -> ((~P1 A e. M /\ ~P1 B e. M) -> E.n e. Nn (A e. n /\ B e. n)))
177	157, 176	syl 15	. 2 |- (M e. Nn -> ((~P1 A e. M /\ ~P1 B e. M) -> E.n e. Nn (A e. n /\ B e. n)))
178	177	3impib 1149	1 |- ((M e. Nn /\ ~P1 A e. M /\ ~P1 B e. M) -> E.n e. Nn (A e. n /\ B e. n))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358   /\ w3a 934  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710  E.wrex 2616  _Vcvv 2860   ∼ ccompl 3206   u. cun 3208  (/)c0 3551  {csn 3738  1_cc1c 4135  ~P₁ cpw1 4136   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-13 1712  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:  tfin11  4494  sfin112  4530  sfindbl  4531  sfinltfin  4536