NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ncfinlower GIF version

Theorem ncfinlower 4483
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 Nn 1A M 1B M) → n Nn (A n B 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.
StepHypRef Expression
1 ncfinlowerlem1 4482 . . . 4 {m ab((1a m 1b m) → n Nn (a n b n))} V
2 eleq2 2414 . . . . . . 7 (m = 0c → (1a m1a 0c))
3 eleq2 2414 . . . . . . 7 (m = 0c → (1b m1b 0c))
42, 3anbi12d 691 . . . . . 6 (m = 0c → ((1a m 1b m) ↔ (1a 0c 1b 0c)))
54imbi1d 308 . . . . 5 (m = 0c → (((1a m 1b m) → n Nn (a n b n)) ↔ ((1a 0c 1b 0c) → n Nn (a n b n))))
652albidv 1627 . . . 4 (m = 0c → (ab((1a m 1b m) → n Nn (a n b n)) ↔ ab((1a 0c 1b 0c) → n Nn (a n b n))))
7 eleq2 2414 . . . . . . 7 (m = k → (1a m1a k))
8 eleq2 2414 . . . . . . 7 (m = k → (1b m1b k))
97, 8anbi12d 691 . . . . . 6 (m = k → ((1a m 1b m) ↔ (1a k 1b k)))
109imbi1d 308 . . . . 5 (m = k → (((1a m 1b m) → n Nn (a n b n)) ↔ ((1a k 1b k) → n Nn (a n b n))))
11102albidv 1627 . . . 4 (m = k → (ab((1a m 1b m) → n Nn (a n b n)) ↔ ab((1a k 1b k) → n Nn (a n b n))))
12 eleq2 2414 . . . . . . 7 (m = (k +c 1c) → (1a m1a (k +c 1c)))
13 eleq2 2414 . . . . . . 7 (m = (k +c 1c) → (1b m1b (k +c 1c)))
1412, 13anbi12d 691 . . . . . 6 (m = (k +c 1c) → ((1a m 1b m) ↔ (1a (k +c 1c) 1b (k +c 1c))))
1514imbi1d 308 . . . . 5 (m = (k +c 1c) → (((1a m 1b m) → n Nn (a n b n)) ↔ ((1a (k +c 1c) 1b (k +c 1c)) → n Nn (a n b n))))
16152albidv 1627 . . . 4 (m = (k +c 1c) → (ab((1a m 1b m) → n Nn (a n b n)) ↔ ab((1a (k +c 1c) 1b (k +c 1c)) → n Nn (a n b n))))
17 eleq2 2414 . . . . . . 7 (m = M → (1a m1a M))
18 eleq2 2414 . . . . . . 7 (m = M → (1b m1b M))
1917, 18anbi12d 691 . . . . . 6 (m = M → ((1a m 1b m) ↔ (1a M 1b M)))
2019imbi1d 308 . . . . 5 (m = M → (((1a m 1b m) → n Nn (a n b n)) ↔ ((1a M 1b M) → n Nn (a n b n))))
21202albidv 1627 . . . 4 (m = M → (ab((1a m 1b m) → n Nn (a n b n)) ↔ ab((1a M 1b M) → n Nn (a n b n))))
22 el0c 4421 . . . . . . 7 (1a 0c1a = )
23 pw10b 4166 . . . . . . 7 (1a = a = )
2422, 23bitri 240 . . . . . 6 (1a 0ca = )
25 el0c 4421 . . . . . . 7 (1b 0c1b = )
26 pw10b 4166 . . . . . . 7 (1b = b = )
2725, 26bitri 240 . . . . . 6 (1b 0cb = )
28 peano1 4402 . . . . . . . 8 0c Nn
29 nulel0c 4422 . . . . . . . 8 0c
30 eleq2 2414 . . . . . . . . 9 (n = 0c → ( n 0c))
3130rspcev 2955 . . . . . . . 8 ((0c Nn 0c) → n Nn n)
3228, 29, 31mp2an 653 . . . . . . 7 n Nn n
33 eleq1 2413 . . . . . . . . . 10 (a = → (a n n))
34 eleq1 2413 . . . . . . . . . 10 (b = → (b n n))
3533, 34bi2anan9 843 . . . . . . . . 9 ((a = b = ) → ((a n b n) ↔ ( n n)))
36 anidm 625 . . . . . . . . 9 (( n n) ↔ n)
3735, 36syl6bb 252 . . . . . . . 8 ((a = b = ) → ((a n b n) ↔ n))
3837rexbidv 2635 . . . . . . 7 ((a = b = ) → (n Nn (a n b n) ↔ n Nn n))
3932, 38mpbiri 224 . . . . . 6 ((a = b = ) → n Nn (a n b n))
4024, 27, 39syl2anb 465 . . . . 5 ((1a 0c 1b 0c) → n Nn (a n b n))
4140gen2 1547 . . . 4 ab((1a 0c 1b 0c) → n Nn (a n b n))
42 nfv 1619 . . . . . . 7 a k Nn
43 nfa1 1788 . . . . . . 7 aab((1a k 1b k) → n Nn (a n b n))
4442, 43nfan 1824 . . . . . 6 a(k Nn ab((1a k 1b k) → n Nn (a n b n)))
45 nfv 1619 . . . . . . . 8 b k Nn
46 nfa2 1855 . . . . . . . 8 bab((1a k 1b k) → n Nn (a n b n))
4745, 46nfan 1824 . . . . . . 7 b(k Nn ab((1a k 1b k) → n Nn (a n b n)))
48 reeanv 2778 . . . . . . . . 9 (c k d k (x c1a = (c ∪ {x}) y d1b = (d ∪ {y})) ↔ (c k x c1a = (c ∪ {x}) d k y d1b = (d ∪ {y})))
49 reeanv 2778 . . . . . . . . . 10 (x cy d(1a = (c ∪ {x}) 1b = (d ∪ {y})) ↔ (x c1a = (c ∪ {x}) y d1b = (d ∪ {y})))
50492rexbii 2641 . . . . . . . . 9 (c k d k x cy d(1a = (c ∪ {x}) 1b = (d ∪ {y})) ↔ c k d k (x c1a = (c ∪ {x}) y d1b = (d ∪ {y})))
51 elsuc 4413 . . . . . . . . . 10 (1a (k +c 1c) ↔ c k x c1a = (c ∪ {x}))
52 elsuc 4413 . . . . . . . . . 10 (1b (k +c 1c) ↔ d k y d1b = (d ∪ {y}))
5351, 52anbi12i 678 . . . . . . . . 9 ((1a (k +c 1c) 1b (k +c 1c)) ↔ (c k x c1a = (c ∪ {x}) d k y d1b = (d ∪ {y})))
5448, 50, 533bitr4ri 269 . . . . . . . 8 ((1a (k +c 1c) 1b (k +c 1c)) ↔ c k d k x cy d(1a = (c ∪ {x}) 1b = (d ∪ {y})))
55 vex 2862 . . . . . . . . . . . . . . . . . . . . . 22 e V
56 vex 2862 . . . . . . . . . . . . . . . . . . . . . 22 f V
57 pw1eq 4143 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a = e1a = 1e)
5857eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . 25 (a = e → (1a k1e k))
59 pw1eq 4143 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b = f1b = 1f)
6059eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . 25 (b = f → (1b k1f k))
6158, 60bi2anan9 843 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a = e b = f) → ((1a k 1b k) ↔ (1e k 1f k)))
62 elequ1 1713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (a = e → (a ne n))
63 elequ1 1713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (b = f → (b nf n))
6462, 63bi2anan9 843 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((a = e b = f) → ((a n b n) ↔ (e n f n)))
6564rexbidv 2635 . . . . . . . . . . . . . . . . . . . . . . . 24 ((a = e b = f) → (n Nn (a n b n) ↔ n Nn (e n f n)))
6661, 65imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . 23 ((a = e b = f) → (((1a k 1b k) → n Nn (a n b n)) ↔ ((1e k 1f k) → n Nn (e n f n))))
6766spc2gv 2942 . . . . . . . . . . . . . . . . . . . . . 22 ((e V f V) → (ab((1a k 1b k) → n Nn (a n b n)) → ((1e k 1f k) → n Nn (e n f n))))
6855, 56, 67mp2an 653 . . . . . . . . . . . . . . . . . . . . 21 (ab((1a k 1b k) → n Nn (a n b n)) → ((1e k 1f k) → n Nn (e n f n)))
6968com12 27 . . . . . . . . . . . . . . . . . . . 20 ((1e k 1f k) → (ab((1a k 1b k) → n Nn (a n b n)) → n Nn (e n f n)))
7069ad2antrl 708 . . . . . . . . . . . . . . . . . . 19 ((k Nn ((1e k 1f k) z e ¬ w f))) → (ab((1a k 1b k) → n Nn (a n b n)) → n Nn (e n f n)))
71 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . 23 (n Nn → (n +c 1c) Nn )
7271ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . 22 (((k Nn ((1e k 1f k) z e ¬ w f))) (n Nn (e n f n))) → (n +c 1c) Nn )
73 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . 23 (((k Nn ((1e k 1f k) z e ¬ w f))) (n Nn (e n f n))) → e n)
74 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . . 24 ((k Nn ((1e k 1f k) z e ¬ w f))) → ¬ z e)
7574adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23 (((k Nn ((1e k 1f k) z e ¬ w f))) (n Nn (e n f n))) → ¬ z e)
76 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . 24 z V
7776elsuci 4414 . . . . . . . . . . . . . . . . . . . . . . 23 ((e n ¬ z e) → (e ∪ {z}) (n +c 1c))
7873, 75, 77syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22 (((k Nn ((1e k 1f k) z e ¬ w f))) (n Nn (e n f n))) → (e ∪ {z}) (n +c 1c))
79 simprrr 741 . . . . . . . . . . . . . . . . . . . . . . 23 (((k Nn ((1e k 1f k) z e ¬ w f))) (n Nn (e n f n))) → f n)
80 simprrr 741 . . . . . . . . . . . . . . . . . . . . . . . 24 ((k Nn ((1e k 1f k) z e ¬ w f))) → ¬ w f)
8180adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23 (((k Nn ((1e k 1f k) z e ¬ w f))) (n Nn (e n f n))) → ¬ w f)
82 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . 24 w V
8382elsuci 4414 . . . . . . . . . . . . . . . . . . . . . . 23 ((f n ¬ w f) → (f ∪ {w}) (n +c 1c))
8479, 81, 83syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22 (((k Nn ((1e k 1f k) z e ¬ w f))) (n Nn (e n f n))) → (f ∪ {w}) (n +c 1c))
85 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . . 24 (m = (n +c 1c) → ((e ∪ {z}) m ↔ (e ∪ {z}) (n +c 1c)))
86 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . . 24 (m = (n +c 1c) → ((f ∪ {w}) m ↔ (f ∪ {w}) (n +c 1c)))
8785, 86anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . 23 (m = (n +c 1c) → (((e ∪ {z}) m (f ∪ {w}) m) ↔ ((e ∪ {z}) (n +c 1c) (f ∪ {w}) (n +c 1c))))
8887rspcev 2955 . . . . . . . . . . . . . . . . . . . . . 22 (((n +c 1c) Nn ((e ∪ {z}) (n +c 1c) (f ∪ {w}) (n +c 1c))) → m Nn ((e ∪ {z}) m (f ∪ {w}) m))
8972, 78, 84, 88syl12anc 1180 . . . . . . . . . . . . . . . . . . . . 21 (((k Nn ((1e k 1f k) z e ¬ w f))) (n Nn (e n f n))) → m Nn ((e ∪ {z}) m (f ∪ {w}) m))
9089expr 598 . . . . . . . . . . . . . . . . . . . 20 (((k Nn ((1e k 1f k) z e ¬ w f))) n Nn ) → ((e n f n) → m Nn ((e ∪ {z}) m (f ∪ {w}) m)))
9190rexlimdva 2738 . . . . . . . . . . . . . . . . . . 19 ((k Nn ((1e k 1f k) z e ¬ w f))) → (n Nn (e n f n) → m Nn ((e ∪ {z}) m (f ∪ {w}) m)))
9270, 91syld 40 . . . . . . . . . . . . . . . . . 18 ((k Nn ((1e k 1f k) z e ¬ w f))) → (ab((1a k 1b k) → n Nn (a n b n)) → m Nn ((e ∪ {z}) m (f ∪ {w}) m)))
9392imp 418 . . . . . . . . . . . . . . . . 17 (((k Nn ((1e k 1f k) z e ¬ w f))) ab((1a k 1b k) → n Nn (a n b n))) → m Nn ((e ∪ {z}) m (f ∪ {w}) m))
9493an32s 779 . . . . . . . . . . . . . . . 16 (((k Nn ab((1a k 1b k) → n Nn (a n b n))) ((1e k 1f k) z e ¬ w f))) → m Nn ((e ∪ {z}) m (f ∪ {w}) m))
95 eleq1 2413 . . . . . . . . . . . . . . . . . . . . 21 (c = 1e → (c k1e k))
96953ad2ant2 977 . . . . . . . . . . . . . . . . . . . 20 ((a = (e ∪ {z}) c = 1e x = {z}) → (c k1e k))
97 eleq1 2413 . . . . . . . . . . . . . . . . . . . . 21 (d = 1f → (d k1f k))
98973ad2ant2 977 . . . . . . . . . . . . . . . . . . . 20 ((b = (f ∪ {w}) d = 1f y = {w}) → (d k1f k))
9996, 98bi2anan9 843 . . . . . . . . . . . . . . . . . . 19 (((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → ((c k d k) ↔ (1e k 1f k)))
100 compleq 3243 . . . . . . . . . . . . . . . . . . . . . . . 24 (c = 1e → ∼ c = ∼ 1e)
101 eleq12 2415 . . . . . . . . . . . . . . . . . . . . . . . 24 ((x = {z} c = ∼ 1e) → (x c ↔ {z} 1e))
102100, 101sylan2 460 . . . . . . . . . . . . . . . . . . . . . . 23 ((x = {z} c = 1e) → (x c ↔ {z} 1e))
103 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . 25 {z} V
104103elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . 24 ({z} 1e ↔ ¬ {z} 1e)
105 snelpw1 4146 . . . . . . . . . . . . . . . . . . . . . . . 24 ({z} 1ez e)
106104, 105xchbinx 301 . . . . . . . . . . . . . . . . . . . . . . 23 ({z} 1e ↔ ¬ z e)
107102, 106syl6bb 252 . . . . . . . . . . . . . . . . . . . . . 22 ((x = {z} c = 1e) → (x c ↔ ¬ z e))
108107ancoms 439 . . . . . . . . . . . . . . . . . . . . 21 ((c = 1e x = {z}) → (x c ↔ ¬ z e))
1091083adant1 973 . . . . . . . . . . . . . . . . . . . 20 ((a = (e ∪ {z}) c = 1e x = {z}) → (x c ↔ ¬ z e))
110 compleq 3243 . . . . . . . . . . . . . . . . . . . . . . . 24 (d = 1f → ∼ d = ∼ 1f)
111 eleq12 2415 . . . . . . . . . . . . . . . . . . . . . . . 24 ((y = {w} d = ∼ 1f) → (y d ↔ {w} 1f))
112110, 111sylan2 460 . . . . . . . . . . . . . . . . . . . . . . 23 ((y = {w} d = 1f) → (y d ↔ {w} 1f))
113 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . 25 {w} V
114113elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . 24 ({w} 1f ↔ ¬ {w} 1f)
115 snelpw1 4146 . . . . . . . . . . . . . . . . . . . . . . . 24 ({w} 1fw f)
116114, 115xchbinx 301 . . . . . . . . . . . . . . . . . . . . . . 23 ({w} 1f ↔ ¬ w f)
117112, 116syl6bb 252 . . . . . . . . . . . . . . . . . . . . . 22 ((y = {w} d = 1f) → (y d ↔ ¬ w f))
118117ancoms 439 . . . . . . . . . . . . . . . . . . . . 21 ((d = 1f y = {w}) → (y d ↔ ¬ w f))
1191183adant1 973 . . . . . . . . . . . . . . . . . . . 20 ((b = (f ∪ {w}) d = 1f y = {w}) → (y d ↔ ¬ w f))
120109, 119bi2anan9 843 . . . . . . . . . . . . . . . . . . 19 (((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → ((x c y d) ↔ (¬ z e ¬ w f)))
12199, 120anbi12d 691 . . . . . . . . . . . . . . . . . 18 (((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → (((c k d k) (x c y d)) ↔ ((1e k 1f k) z e ¬ w f))))
122121anbi2d 684 . . . . . . . . . . . . . . . . 17 (((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → (((k Nn ab((1a k 1b k) → n Nn (a n b n))) ((c k d k) (x c y d))) ↔ ((k Nn ab((1a k 1b k) → n Nn (a n b n))) ((1e k 1f k) z e ¬ w f)))))
123 eleq1 2413 . . . . . . . . . . . . . . . . . . . 20 (a = (e ∪ {z}) → (a m ↔ (e ∪ {z}) m))
1241233ad2ant1 976 . . . . . . . . . . . . . . . . . . 19 ((a = (e ∪ {z}) c = 1e x = {z}) → (a m ↔ (e ∪ {z}) m))
125 eleq1 2413 . . . . . . . . . . . . . . . . . . . 20 (b = (f ∪ {w}) → (b m ↔ (f ∪ {w}) m))
1261253ad2ant1 976 . . . . . . . . . . . . . . . . . . 19 ((b = (f ∪ {w}) d = 1f y = {w}) → (b m ↔ (f ∪ {w}) m))
127124, 126bi2anan9 843 . . . . . . . . . . . . . . . . . 18 (((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → ((a m b m) ↔ ((e ∪ {z}) m (f ∪ {w}) m)))
128127rexbidv 2635 . . . . . . . . . . . . . . . . 17 (((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → (m Nn (a m b m) ↔ m Nn ((e ∪ {z}) m (f ∪ {w}) m)))
129122, 128imbi12d 311 . . . . . . . . . . . . . . . 16 (((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → ((((k Nn ab((1a k 1b k) → n Nn (a n b n))) ((c k d k) (x c y d))) → m Nn (a m b m)) ↔ (((k Nn ab((1a k 1b k) → n Nn (a n b n))) ((1e k 1f k) z e ¬ w f))) → m Nn ((e ∪ {z}) m (f ∪ {w}) m))))
13094, 129mpbiri 224 . . . . . . . . . . . . . . 15 (((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → (((k Nn ab((1a k 1b k) → n Nn (a n b n))) ((c k d k) (x c y d))) → m Nn (a m b m)))
131130com12 27 . . . . . . . . . . . . . 14 (((k Nn ab((1a k 1b k) → n Nn (a n b n))) ((c k d k) (x c y d))) → (((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → m Nn (a m b m)))
132131exlimdvv 1637 . . . . . . . . . . . . 13 (((k Nn ab((1a k 1b k) → n Nn (a n b n))) ((c k d k) (x c y d))) → (zw((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → m Nn (a m b m)))
133132exlimdvv 1637 . . . . . . . . . . . 12 (((k Nn ab((1a k 1b k) → n Nn (a n b n))) ((c k d k) (x c y d))) → (efzw((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) → m Nn (a m b m)))
134 eeanv 1913 . . . . . . . . . . . . 13 (ef(z(a = (e ∪ {z}) c = 1e x = {z}) w(b = (f ∪ {w}) d = 1f y = {w})) ↔ (ez(a = (e ∪ {z}) c = 1e x = {z}) fw(b = (f ∪ {w}) d = 1f y = {w})))
135 eeanv 1913 . . . . . . . . . . . . . 14 (zw((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) ↔ (z(a = (e ∪ {z}) c = 1e x = {z}) w(b = (f ∪ {w}) d = 1f y = {w})))
1361352exbii 1583 . . . . . . . . . . . . 13 (efzw((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})) ↔ ef(z(a = (e ∪ {z}) c = 1e x = {z}) w(b = (f ∪ {w}) d = 1f y = {w})))
137 vex 2862 . . . . . . . . . . . . . . 15 c V
138 vex 2862 . . . . . . . . . . . . . . 15 x V
139137, 138pw1eqadj 4332 . . . . . . . . . . . . . 14 (1a = (c ∪ {x}) ↔ ez(a = (e ∪ {z}) c = 1e x = {z}))
140 vex 2862 . . . . . . . . . . . . . . 15 d V
141 vex 2862 . . . . . . . . . . . . . . 15 y V
142140, 141pw1eqadj 4332 . . . . . . . . . . . . . 14 (1b = (d ∪ {y}) ↔ fw(b = (f ∪ {w}) d = 1f y = {w}))
143139, 142anbi12i 678 . . . . . . . . . . . . 13 ((1a = (c ∪ {x}) 1b = (d ∪ {y})) ↔ (ez(a = (e ∪ {z}) c = 1e x = {z}) fw(b = (f ∪ {w}) d = 1f y = {w})))
144134, 136, 1433bitr4ri 269 . . . . . . . . . . . 12 ((1a = (c ∪ {x}) 1b = (d ∪ {y})) ↔ efzw((a = (e ∪ {z}) c = 1e x = {z}) (b = (f ∪ {w}) d = 1f y = {w})))
145 elequ2 1715 . . . . . . . . . . . . . 14 (n = m → (a na m))
146 elequ2 1715 . . . . . . . . . . . . . 14 (n = m → (b nb m))
147145, 146anbi12d 691 . . . . . . . . . . . . 13 (n = m → ((a n b n) ↔ (a m b m)))
148147cbvrexv 2836 . . . . . . . . . . . 12 (n Nn (a n b n) ↔ m Nn (a m b m))
149133, 144, 1483imtr4g 261 . . . . . . . . . . 11 (((k Nn ab((1a k 1b k) → n Nn (a n b n))) ((c k d k) (x c y d))) → ((1a = (c ∪ {x}) 1b = (d ∪ {y})) → n Nn (a n b n)))
150149expr 598 . . . . . . . . . 10 (((k Nn ab((1a k 1b k) → n Nn (a n b n))) (c k d k)) → ((x c y d) → ((1a = (c ∪ {x}) 1b = (d ∪ {y})) → n Nn (a n b n))))
151150rexlimdvv 2744 . . . . . . . . 9 (((k Nn ab((1a k 1b k) → n Nn (a n b n))) (c k d k)) → (x cy d(1a = (c ∪ {x}) 1b = (d ∪ {y})) → n Nn (a n b n)))
152151rexlimdvva 2745 . . . . . . . 8 ((k Nn ab((1a k 1b k) → n Nn (a n b n))) → (c k d k x cy d(1a = (c ∪ {x}) 1b = (d ∪ {y})) → n Nn (a n b n)))
15354, 152syl5bi 208 . . . . . . 7 ((k Nn ab((1a k 1b k) → n Nn (a n b n))) → ((1a (k +c 1c) 1b (k +c 1c)) → n Nn (a n b n)))
15447, 153alrimi 1765 . . . . . 6 ((k Nn ab((1a k 1b k) → n Nn (a n b n))) → b((1a (k +c 1c) 1b (k +c 1c)) → n Nn (a n b n)))
15544, 154alrimi 1765 . . . . 5 ((k Nn ab((1a k 1b k) → n Nn (a n b n))) → ab((1a (k +c 1c) 1b (k +c 1c)) → n Nn (a n b n)))
156155ex 423 . . . 4 (k Nn → (ab((1a k 1b k) → n Nn (a n b n)) → ab((1a (k +c 1c) 1b (k +c 1c)) → n Nn (a n b n))))
1571, 6, 11, 16, 21, 41, 156finds 4411 . . 3 (M Nnab((1a M 1b M) → n Nn (a n b n)))
158 elex 2867 . . . . . 6 (1A M1A V)
159 pw1exb 4326 . . . . . 6 (1A V ↔ A V)
160158, 159sylib 188 . . . . 5 (1A MA V)
161 elex 2867 . . . . . 6 (1B M1B V)
162 pw1exb 4326 . . . . . 6 (1B V ↔ B V)
163161, 162sylib 188 . . . . 5 (1B MB V)
164 pw1eq 4143 . . . . . . . . 9 (a = A1a = 1A)
165164eleq1d 2419 . . . . . . . 8 (a = A → (1a M1A M))
166 pw1eq 4143 . . . . . . . . 9 (b = B1b = 1B)
167166eleq1d 2419 . . . . . . . 8 (b = B → (1b M1B M))
168165, 167bi2anan9 843 . . . . . . 7 ((a = A b = B) → ((1a M 1b M) ↔ (1A M 1B M)))
169 eleq1 2413 . . . . . . . . 9 (a = A → (a nA n))
170 eleq1 2413 . . . . . . . . 9 (b = B → (b nB n))
171169, 170bi2anan9 843 . . . . . . . 8 ((a = A b = B) → ((a n b n) ↔ (A n B n)))
172171rexbidv 2635 . . . . . . 7 ((a = A b = B) → (n Nn (a n b n) ↔ n Nn (A n B n)))
173168, 172imbi12d 311 . . . . . 6 ((a = A b = B) → (((1a M 1b M) → n Nn (a n b n)) ↔ ((1A M 1B M) → n Nn (A n B n))))
174173spc2gv 2942 . . . . 5 ((A V B V) → (ab((1a M 1b M) → n Nn (a n b n)) → ((1A M 1B M) → n Nn (A n B n))))
175160, 163, 174syl2an 463 . . . 4 ((1A M 1B M) → (ab((1a M 1b M) → n Nn (a n b n)) → ((1A M 1B M) → n Nn (A n B n))))
176175pm2.43b 46 . . 3 (ab((1a M 1b M) → n Nn (a n b n)) → ((1A M 1B M) → n Nn (A n B n)))
177157, 176syl 15 . 2 (M Nn → ((1A M 1B M) → n Nn (A n B n)))
1781773impib 1149 1 ((M Nn 1A M 1B M) → n Nn (A n B n))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wa 358   w3a 934  wal 1540  wex 1541   = wceq 1642   wcel 1710  wrex 2615  Vcvv 2859  ccompl 3205  cun 3207  c0 3550  {csn 3737  1cc1c 4134  1cpw1 4135   Nn cnnc 4373  0cc0c 4374   +c 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-13 1712  ax-14 1714  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:  tfin11  4493  sfin112  4529  sfindbl  4530  sfinltfin  4535
  Copyright terms: Public domain W3C validator