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

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 Nn A M B M) → n Nn (1A n 1B 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.
StepHypRef Expression
1 ncfinraiselem2 4480 . . . 4 {m a m b m n Nn (1a n 1b n)} V
2 raleq 2807 . . . . 5 (m = 0c → (b m n Nn (1a n 1b n) ↔ b 0c n Nn (1a n 1b n)))
32raleqbi1dv 2815 . . . 4 (m = 0c → (a m b m n Nn (1a n 1b n) ↔ a 0c b 0c n Nn (1a n 1b n)))
4 raleq 2807 . . . . 5 (m = k → (b m n Nn (1a n 1b n) ↔ b k n Nn (1a n 1b n)))
54raleqbi1dv 2815 . . . 4 (m = k → (a m b m n Nn (1a n 1b n) ↔ a k b k n Nn (1a n 1b n)))
6 raleq 2807 . . . . 5 (m = (k +c 1c) → (b m n Nn (1a n 1b n) ↔ b (k +c 1c)n Nn (1a n 1b n)))
76raleqbi1dv 2815 . . . 4 (m = (k +c 1c) → (a m b m n Nn (1a n 1b n) ↔ a (k +c 1c)b (k +c 1c)n Nn (1a n 1b n)))
8 raleq 2807 . . . . 5 (m = M → (b m n Nn (1a n 1b n) ↔ b M n Nn (1a n 1b n)))
98raleqbi1dv 2815 . . . 4 (m = M → (a m b m n Nn (1a n 1b n) ↔ a M b M n Nn (1a n 1b n)))
10 el0c 4421 . . . . . 6 (a 0ca = )
11 el0c 4421 . . . . . 6 (b 0cb = )
12 peano1 4402 . . . . . . . 8 0c Nn
13 nulel0c 4422 . . . . . . . . 9 0c
1413, 13pm3.2i 441 . . . . . . . 8 ( 0c 0c)
15 eleq2 2414 . . . . . . . . . 10 (n = 0c → ( n 0c))
1615, 15anbi12d 691 . . . . . . . . 9 (n = 0c → (( n n) ↔ ( 0c 0c)))
1716rspcev 2955 . . . . . . . 8 ((0c Nn ( 0c 0c)) → n Nn ( n n))
1812, 14, 17mp2an 653 . . . . . . 7 n Nn ( n n)
19 pw1eq 4143 . . . . . . . . . . 11 (a = 1a = 1)
20 pw10 4161 . . . . . . . . . . 11 1 =
2119, 20syl6eq 2401 . . . . . . . . . 10 (a = 1a = )
2221eleq1d 2419 . . . . . . . . 9 (a = → (1a n n))
23 pw1eq 4143 . . . . . . . . . . 11 (b = 1b = 1)
2423, 20syl6eq 2401 . . . . . . . . . 10 (b = 1b = )
2524eleq1d 2419 . . . . . . . . 9 (b = → (1b n n))
2622, 25bi2anan9 843 . . . . . . . 8 ((a = b = ) → ((1a n 1b n) ↔ ( n n)))
2726rexbidv 2635 . . . . . . 7 ((a = b = ) → (n Nn (1a n 1b n) ↔ n Nn ( n n)))
2818, 27mpbiri 224 . . . . . 6 ((a = b = ) → n Nn (1a n 1b n))
2910, 11, 28syl2anb 465 . . . . 5 ((a 0c b 0c) → n Nn (1a n 1b n))
3029rgen2a 2680 . . . 4 a 0c b 0c n Nn (1a n 1b n)
31 nfv 1619 . . . . . . 7 a k Nn
32 nfra1 2664 . . . . . . 7 aa k b k n Nn (1a n 1b n)
3331, 32nfan 1824 . . . . . 6 a(k Nn a k b k n Nn (1a n 1b n))
34 nfv 1619 . . . . . . . 8 b k Nn
35 nfra2 2668 . . . . . . . 8 ba k b k n Nn (1a n 1b n)
3634, 35nfan 1824 . . . . . . 7 b(k Nn a k b k n Nn (1a n 1b n))
37 nfv 1619 . . . . . . 7 b a (k +c 1c)
38 reeanv 2778 . . . . . . . . . 10 (c k d k (x ca = (c ∪ {x}) y db = (d ∪ {y})) ↔ (c k x ca = (c ∪ {x}) d k y db = (d ∪ {y})))
39 reeanv 2778 . . . . . . . . . . 11 (x cy d(a = (c ∪ {x}) b = (d ∪ {y})) ↔ (x ca = (c ∪ {x}) y db = (d ∪ {y})))
40392rexbii 2641 . . . . . . . . . 10 (c k d k x cy d(a = (c ∪ {x}) b = (d ∪ {y})) ↔ c k d k (x ca = (c ∪ {x}) y db = (d ∪ {y})))
41 elsuc 4413 . . . . . . . . . . 11 (a (k +c 1c) ↔ c k x ca = (c ∪ {x}))
42 elsuc 4413 . . . . . . . . . . 11 (b (k +c 1c) ↔ d k y db = (d ∪ {y}))
4341, 42anbi12i 678 . . . . . . . . . 10 ((a (k +c 1c) b (k +c 1c)) ↔ (c k x ca = (c ∪ {x}) d k y db = (d ∪ {y})))
4438, 40, 433bitr4ri 269 . . . . . . . . 9 ((a (k +c 1c) b (k +c 1c)) ↔ c k d k x cy d(a = (c ∪ {x}) b = (d ∪ {y})))
45 pw1eq 4143 . . . . . . . . . . . . . . . . 17 (a = c1a = 1c)
4645eleq1d 2419 . . . . . . . . . . . . . . . 16 (a = c → (1a n1c n))
4746anbi1d 685 . . . . . . . . . . . . . . 15 (a = c → ((1a n 1b n) ↔ (1c n 1b n)))
4847rexbidv 2635 . . . . . . . . . . . . . 14 (a = c → (n Nn (1a n 1b n) ↔ n Nn (1c n 1b n)))
49 pw1eq 4143 . . . . . . . . . . . . . . . . 17 (b = d1b = 1d)
5049eleq1d 2419 . . . . . . . . . . . . . . . 16 (b = d → (1b n1d n))
5150anbi2d 684 . . . . . . . . . . . . . . 15 (b = d → ((1c n 1b n) ↔ (1c n 1d n)))
5251rexbidv 2635 . . . . . . . . . . . . . 14 (b = d → (n Nn (1c n 1b n) ↔ n Nn (1c n 1d n)))
5348, 52rspc2v 2961 . . . . . . . . . . . . 13 ((c k d k) → (a k b k n Nn (1a n 1b n) → n Nn (1c n 1d n)))
5453com12 27 . . . . . . . . . . . 12 (a k b k n Nn (1a n 1b n) → ((c k d k) → n Nn (1c n 1d n)))
55 vex 2862 . . . . . . . . . . . . . . . . . . . 20 x V
5655elcompl 3225 . . . . . . . . . . . . . . . . . . 19 (x c ↔ ¬ x c)
57 vex 2862 . . . . . . . . . . . . . . . . . . . 20 y V
5857elcompl 3225 . . . . . . . . . . . . . . . . . . 19 (y d ↔ ¬ y d)
5956, 58anbi12i 678 . . . . . . . . . . . . . . . . . 18 ((x c y d) ↔ (¬ x c ¬ y d))
6059anbi2i 675 . . . . . . . . . . . . . . . . 17 (((c k d k) (x c y d)) ↔ ((c k d k) x c ¬ y d)))
61 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (n Nn → (n +c 1c) Nn )
6261ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((n Nn (1c n 1d n)) k Nn ) ((c k d k) x c ¬ y d))) → (n +c 1c) Nn )
63 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((n Nn (1c n 1d n)) k Nn ) → 1c n)
6463adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((n Nn (1c n 1d n)) k Nn ) ((c k d k) x c ¬ y d))) → 1c n)
65 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((n Nn (1c n 1d n)) k Nn ) ((c k d k) x c ¬ y d))) → ¬ x c)
66 snelpw1 4146 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({x} 1cx c)
6765, 66sylnibr 296 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((n Nn (1c n 1d n)) k Nn ) ((c k d k) x c ¬ y d))) → ¬ {x} 1c)
68 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {x} V
6968elsuci 4414 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1c n ¬ {x} 1c) → (1c ∪ {{x}}) (n +c 1c))
7064, 67, 69syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((n Nn (1c n 1d n)) k Nn ) ((c k d k) x c ¬ y d))) → (1c ∪ {{x}}) (n +c 1c))
71 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((n Nn (1c n 1d n)) k Nn ) → 1d n)
7271adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((n Nn (1c n 1d n)) k Nn ) ((c k d k) x c ¬ y d))) → 1d n)
73 simprrr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((n Nn (1c n 1d n)) k Nn ) ((c k d k) x c ¬ y d))) → ¬ y d)
74 snelpw1 4146 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({y} 1dy d)
7573, 74sylnibr 296 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((n Nn (1c n 1d n)) k Nn ) ((c k d k) x c ¬ y d))) → ¬ {y} 1d)
76 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {y} V
7776elsuci 4414 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1d n ¬ {y} 1d) → (1d ∪ {{y}}) (n +c 1c))
7872, 75, 77syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((n Nn (1c n 1d n)) k Nn ) ((c k d k) x c ¬ y d))) → (1d ∪ {{y}}) (n +c 1c))
79 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (m = (n +c 1c) → ((1c ∪ {{x}}) m ↔ (1c ∪ {{x}}) (n +c 1c)))
80 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (m = (n +c 1c) → ((1d ∪ {{y}}) m ↔ (1d ∪ {{y}}) (n +c 1c)))
8179, 80anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (m = (n +c 1c) → (((1c ∪ {{x}}) m (1d ∪ {{y}}) m) ↔ ((1c ∪ {{x}}) (n +c 1c) (1d ∪ {{y}}) (n +c 1c))))
8281rspcev 2955 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((n +c 1c) Nn ((1c ∪ {{x}}) (n +c 1c) (1d ∪ {{y}}) (n +c 1c))) → m Nn ((1c ∪ {{x}}) m (1d ∪ {{y}}) m))
8362, 70, 78, 82syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((n Nn (1c n 1d n)) k Nn ) ((c k d k) x c ¬ y d))) → m Nn ((1c ∪ {{x}}) m (1d ∪ {{y}}) m))
8483ex 423 . . . . . . . . . . . . . . . . . . . . . . 23 (((n Nn (1c n 1d n)) k Nn ) → (((c k d k) x c ¬ y d)) → m Nn ((1c ∪ {{x}}) m (1d ∪ {{y}}) m)))
8584ex 423 . . . . . . . . . . . . . . . . . . . . . 22 ((n Nn (1c n 1d n)) → (k Nn → (((c k d k) x c ¬ y d)) → m Nn ((1c ∪ {{x}}) m (1d ∪ {{y}}) m))))
8685rexlimiva 2733 . . . . . . . . . . . . . . . . . . . . 21 (n Nn (1c n 1d n) → (k Nn → (((c k d k) x c ¬ y d)) → m Nn ((1c ∪ {{x}}) m (1d ∪ {{y}}) m))))
87 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . 23 (m = n → ((1c ∪ {{x}}) m ↔ (1c ∪ {{x}}) n))
88 eleq2 2414 . . . . . . . . . . . . . . . . . . . . . . 23 (m = n → ((1d ∪ {{y}}) m ↔ (1d ∪ {{y}}) n))
8987, 88anbi12d 691 . . . . . . . . . . . . . . . . . . . . . 22 (m = n → (((1c ∪ {{x}}) m (1d ∪ {{y}}) m) ↔ ((1c ∪ {{x}}) n (1d ∪ {{y}}) n)))
9089cbvrexv 2836 . . . . . . . . . . . . . . . . . . . . 21 (m Nn ((1c ∪ {{x}}) m (1d ∪ {{y}}) m) ↔ n Nn ((1c ∪ {{x}}) n (1d ∪ {{y}}) n))
9186, 90syl8ib 222 . . . . . . . . . . . . . . . . . . . 20 (n Nn (1c n 1d n) → (k Nn → (((c k d k) x c ¬ y d)) → n Nn ((1c ∪ {{x}}) n (1d ∪ {{y}}) n))))
9291com12 27 . . . . . . . . . . . . . . . . . . 19 (k Nn → (n Nn (1c n 1d n) → (((c k d k) x c ¬ y d)) → n Nn ((1c ∪ {{x}}) n (1d ∪ {{y}}) n))))
9392imp31 421 . . . . . . . . . . . . . . . . . 18 (((k Nn n Nn (1c n 1d n)) ((c k d k) x c ¬ y d))) → n Nn ((1c ∪ {{x}}) n (1d ∪ {{y}}) n))
94 pw1eq 4143 . . . . . . . . . . . . . . . . . . . . . 22 (a = (c ∪ {x}) → 1a = 1(c ∪ {x}))
95 pw1un 4163 . . . . . . . . . . . . . . . . . . . . . . 23 1(c ∪ {x}) = (1c1{x})
9655pw1sn 4165 . . . . . . . . . . . . . . . . . . . . . . . 24 1{x} = {{x}}
9796uneq2i 3415 . . . . . . . . . . . . . . . . . . . . . . 23 (1c1{x}) = (1c ∪ {{x}})
9895, 97eqtri 2373 . . . . . . . . . . . . . . . . . . . . . 22 1(c ∪ {x}) = (1c ∪ {{x}})
9994, 98syl6eq 2401 . . . . . . . . . . . . . . . . . . . . 21 (a = (c ∪ {x}) → 1a = (1c ∪ {{x}}))
10099eleq1d 2419 . . . . . . . . . . . . . . . . . . . 20 (a = (c ∪ {x}) → (1a n ↔ (1c ∪ {{x}}) n))
101 pw1eq 4143 . . . . . . . . . . . . . . . . . . . . . 22 (b = (d ∪ {y}) → 1b = 1(d ∪ {y}))
102 pw1un 4163 . . . . . . . . . . . . . . . . . . . . . . 23 1(d ∪ {y}) = (1d1{y})
10357pw1sn 4165 . . . . . . . . . . . . . . . . . . . . . . . 24 1{y} = {{y}}
104103uneq2i 3415 . . . . . . . . . . . . . . . . . . . . . . 23 (1d1{y}) = (1d ∪ {{y}})
105102, 104eqtri 2373 . . . . . . . . . . . . . . . . . . . . . 22 1(d ∪ {y}) = (1d ∪ {{y}})
106101, 105syl6eq 2401 . . . . . . . . . . . . . . . . . . . . 21 (b = (d ∪ {y}) → 1b = (1d ∪ {{y}}))
107106eleq1d 2419 . . . . . . . . . . . . . . . . . . . 20 (b = (d ∪ {y}) → (1b n ↔ (1d ∪ {{y}}) n))
108100, 107bi2anan9 843 . . . . . . . . . . . . . . . . . . 19 ((a = (c ∪ {x}) b = (d ∪ {y})) → ((1a n 1b n) ↔ ((1c ∪ {{x}}) n (1d ∪ {{y}}) n)))
109108rexbidv 2635 . . . . . . . . . . . . . . . . . 18 ((a = (c ∪ {x}) b = (d ∪ {y})) → (n Nn (1a n 1b n) ↔ n Nn ((1c ∪ {{x}}) n (1d ∪ {{y}}) n)))
11093, 109syl5ibrcom 213 . . . . . . . . . . . . . . . . 17 (((k Nn n Nn (1c n 1d n)) ((c k d k) x c ¬ y d))) → ((a = (c ∪ {x}) b = (d ∪ {y})) → n Nn (1a n 1b n)))
11160, 110sylan2b 461 . . . . . . . . . . . . . . . 16 (((k Nn n Nn (1c n 1d n)) ((c k d k) (x c y d))) → ((a = (c ∪ {x}) b = (d ∪ {y})) → n Nn (1a n 1b n)))
112111expr 598 . . . . . . . . . . . . . . 15 (((k Nn n Nn (1c n 1d n)) (c k d k)) → ((x c y d) → ((a = (c ∪ {x}) b = (d ∪ {y})) → n Nn (1a n 1b n))))
113112anasss 628 . . . . . . . . . . . . . 14 ((k Nn (n Nn (1c n 1d n) (c k d k))) → ((x c y d) → ((a = (c ∪ {x}) b = (d ∪ {y})) → n Nn (1a n 1b n))))
114113rexlimdvv 2744 . . . . . . . . . . . . 13 ((k Nn (n Nn (1c n 1d n) (c k d k))) → (x cy d(a = (c ∪ {x}) b = (d ∪ {y})) → n Nn (1a n 1b n)))
115114exp32 588 . . . . . . . . . . . 12 (k Nn → (n Nn (1c n 1d n) → ((c k d k) → (x cy d(a = (c ∪ {x}) b = (d ∪ {y})) → n Nn (1a n 1b n)))))
11654, 115sylan9r 639 . . . . . . . . . . 11 ((k Nn a k b k n Nn (1a n 1b n)) → ((c k d k) → ((c k d k) → (x cy d(a = (c ∪ {x}) b = (d ∪ {y})) → n Nn (1a n 1b n)))))
117116pm2.43d 44 . . . . . . . . . 10 ((k Nn a k b k n Nn (1a n 1b n)) → ((c k d k) → (x cy d(a = (c ∪ {x}) b = (d ∪ {y})) → n Nn (1a n 1b n))))
118117rexlimdvv 2744 . . . . . . . . 9 ((k Nn a k b k n Nn (1a n 1b n)) → (c k d k x cy d(a = (c ∪ {x}) b = (d ∪ {y})) → n Nn (1a n 1b n)))
11944, 118syl5bi 208 . . . . . . . 8 ((k Nn a k b k n Nn (1a n 1b n)) → ((a (k +c 1c) b (k +c 1c)) → n Nn (1a n 1b n)))
120119exp3a 425 . . . . . . 7 ((k Nn a k b k n Nn (1a n 1b n)) → (a (k +c 1c) → (b (k +c 1c) → n Nn (1a n 1b n))))
12136, 37, 120ralrimd 2702 . . . . . 6 ((k Nn a k b k n Nn (1a n 1b n)) → (a (k +c 1c) → b (k +c 1c)n Nn (1a n 1b n)))
12233, 121ralrimi 2695 . . . . 5 ((k Nn a k b k n Nn (1a n 1b n)) → a (k +c 1c)b (k +c 1c)n Nn (1a n 1b n))
123122ex 423 . . . 4 (k Nn → (a k b k n Nn (1a n 1b n) → a (k +c 1c)b (k +c 1c)n Nn (1a n 1b n)))
1241, 3, 5, 7, 9, 30, 123finds 4411 . . 3 (M Nna M b M n Nn (1a n 1b n))
125 pw1eq 4143 . . . . . . 7 (a = A1a = 1A)
126125eleq1d 2419 . . . . . 6 (a = A → (1a n1A n))
127126anbi1d 685 . . . . 5 (a = A → ((1a n 1b n) ↔ (1A n 1b n)))
128127rexbidv 2635 . . . 4 (a = A → (n Nn (1a n 1b n) ↔ n Nn (1A n 1b n)))
129 pw1eq 4143 . . . . . . 7 (b = B1b = 1B)
130129eleq1d 2419 . . . . . 6 (b = B → (1b n1B n))
131130anbi2d 684 . . . . 5 (b = B → ((1A n 1b n) ↔ (1A n 1B n)))
132131rexbidv 2635 . . . 4 (b = B → (n Nn (1A n 1b n) ↔ n Nn (1A n 1B n)))
133128, 132rspc2v 2961 . . 3 ((A M B M) → (a M b M n Nn (1a n 1b n) → n Nn (1A n 1B n)))
134124, 133syl5com 26 . 2 (M Nn → ((A M B M) → n Nn (1A n 1B n)))
1351343impib 1149 1 ((M Nn A M B M) → n Nn (1A n 1B n))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   wa 358   w3a 934   = wceq 1642   wcel 1710  wral 2614  wrex 2615  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-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
  Copyright terms: Public domain W3C validator