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

Theorem nnsucelr 4428
Description: Transfer membership in the successor of a natural into membership of the natural itself. Theorem X.1.17 of [Rosser] p. 525. (Contributed by SF, 14-Jan-2015.)
Hypotheses
Ref Expression
nnsucelr.1 A V
nnsucelr.2 X V
Assertion
Ref Expression
nnsucelr ((M Nn X A (A ∪ {X}) (M +c 1c))) → A M)

Proof of Theorem nnsucelr
Dummy variables a c m n x y z b d w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnsucelrlem1 4424 . . . 4 {m ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m)} V
2 addceq1 4383 . . . . . . . . . 10 (m = 0c → (m +c 1c) = (0c +c 1c))
3 addcid2 4407 . . . . . . . . . 10 (0c +c 1c) = 1c
42, 3syl6eq 2401 . . . . . . . . 9 (m = 0c → (m +c 1c) = 1c)
54eleq2d 2420 . . . . . . . 8 (m = 0c → ((a ∪ {x}) (m +c 1c) ↔ (a ∪ {x}) 1c))
6 el1c 4139 . . . . . . . 8 ((a ∪ {x}) 1cy(a ∪ {x}) = {y})
75, 6syl6bb 252 . . . . . . 7 (m = 0c → ((a ∪ {x}) (m +c 1c) ↔ y(a ∪ {x}) = {y}))
87anbi2d 684 . . . . . 6 (m = 0c → ((¬ x a (a ∪ {x}) (m +c 1c)) ↔ (¬ x a y(a ∪ {x}) = {y})))
9 eleq2 2414 . . . . . . 7 (m = 0c → (a ma 0c))
10 df-0c 4377 . . . . . . . . 9 0c = {}
1110eleq2i 2417 . . . . . . . 8 (a 0ca {})
12 vex 2862 . . . . . . . . 9 a V
1312elsnc 3756 . . . . . . . 8 (a {} ↔ a = )
1411, 13bitri 240 . . . . . . 7 (a 0ca = )
159, 14syl6bb 252 . . . . . 6 (m = 0c → (a ma = ))
168, 15imbi12d 311 . . . . 5 (m = 0c → (((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ ((¬ x a y(a ∪ {x}) = {y}) → a = )))
17162albidv 1627 . . . 4 (m = 0c → (ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ ax((¬ x a y(a ∪ {x}) = {y}) → a = )))
18 addceq1 4383 . . . . . . . . 9 (m = n → (m +c 1c) = (n +c 1c))
1918eleq2d 2420 . . . . . . . 8 (m = n → ((a ∪ {x}) (m +c 1c) ↔ (a ∪ {x}) (n +c 1c)))
2019anbi2d 684 . . . . . . 7 (m = n → ((¬ x a (a ∪ {x}) (m +c 1c)) ↔ (¬ x a (a ∪ {x}) (n +c 1c))))
21 eleq2 2414 . . . . . . 7 (m = n → (a ma n))
2220, 21imbi12d 311 . . . . . 6 (m = n → (((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ ((¬ x a (a ∪ {x}) (n +c 1c)) → a n)))
23222albidv 1627 . . . . 5 (m = n → (ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ ax((¬ x a (a ∪ {x}) (n +c 1c)) → a n)))
24 eleq12 2415 . . . . . . . . . 10 ((x = z a = c) → (x az c))
2524ancoms 439 . . . . . . . . 9 ((a = c x = z) → (x az c))
2625notbid 285 . . . . . . . 8 ((a = c x = z) → (¬ x a ↔ ¬ z c))
27 sneq 3744 . . . . . . . . . 10 (x = z → {x} = {z})
28 uneq12 3413 . . . . . . . . . 10 ((a = c {x} = {z}) → (a ∪ {x}) = (c ∪ {z}))
2927, 28sylan2 460 . . . . . . . . 9 ((a = c x = z) → (a ∪ {x}) = (c ∪ {z}))
3029eleq1d 2419 . . . . . . . 8 ((a = c x = z) → ((a ∪ {x}) (n +c 1c) ↔ (c ∪ {z}) (n +c 1c)))
3126, 30anbi12d 691 . . . . . . 7 ((a = c x = z) → ((¬ x a (a ∪ {x}) (n +c 1c)) ↔ (¬ z c (c ∪ {z}) (n +c 1c))))
32 eleq1 2413 . . . . . . . 8 (a = c → (a nc n))
3332adantr 451 . . . . . . 7 ((a = c x = z) → (a nc n))
3431, 33imbi12d 311 . . . . . 6 ((a = c x = z) → (((¬ x a (a ∪ {x}) (n +c 1c)) → a n) ↔ ((¬ z c (c ∪ {z}) (n +c 1c)) → c n)))
3534cbval2v 2006 . . . . 5 (ax((¬ x a (a ∪ {x}) (n +c 1c)) → a n) ↔ cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n))
3623, 35syl6bb 252 . . . 4 (m = n → (ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n)))
37 addceq1 4383 . . . . . . . 8 (m = (n +c 1c) → (m +c 1c) = ((n +c 1c) +c 1c))
3837eleq2d 2420 . . . . . . 7 (m = (n +c 1c) → ((a ∪ {x}) (m +c 1c) ↔ (a ∪ {x}) ((n +c 1c) +c 1c)))
3938anbi2d 684 . . . . . 6 (m = (n +c 1c) → ((¬ x a (a ∪ {x}) (m +c 1c)) ↔ (¬ x a (a ∪ {x}) ((n +c 1c) +c 1c))))
40 eleq2 2414 . . . . . 6 (m = (n +c 1c) → (a ma (n +c 1c)))
4139, 40imbi12d 311 . . . . 5 (m = (n +c 1c) → (((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ ((¬ x a (a ∪ {x}) ((n +c 1c) +c 1c)) → a (n +c 1c))))
42412albidv 1627 . . . 4 (m = (n +c 1c) → (ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ ax((¬ x a (a ∪ {x}) ((n +c 1c) +c 1c)) → a (n +c 1c))))
43 addceq1 4383 . . . . . . . 8 (m = M → (m +c 1c) = (M +c 1c))
4443eleq2d 2420 . . . . . . 7 (m = M → ((a ∪ {x}) (m +c 1c) ↔ (a ∪ {x}) (M +c 1c)))
4544anbi2d 684 . . . . . 6 (m = M → ((¬ x a (a ∪ {x}) (m +c 1c)) ↔ (¬ x a (a ∪ {x}) (M +c 1c))))
46 eleq2 2414 . . . . . 6 (m = M → (a ma M))
4745, 46imbi12d 311 . . . . 5 (m = M → (((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ ((¬ x a (a ∪ {x}) (M +c 1c)) → a M)))
48472albidv 1627 . . . 4 (m = M → (ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m) ↔ ax((¬ x a (a ∪ {x}) (M +c 1c)) → a M)))
49 vex 2862 . . . . . . . . . . 11 x V
5049unsneqsn 3887 . . . . . . . . . 10 ((a ∪ {x}) = {y} → (a = a = {x}))
5150ord 366 . . . . . . . . 9 ((a ∪ {x}) = {y} → (¬ a = a = {x}))
5249snid 3760 . . . . . . . . . 10 x {x}
53 eleq2 2414 . . . . . . . . . 10 (a = {x} → (x ax {x}))
5452, 53mpbiri 224 . . . . . . . . 9 (a = {x} → x a)
5551, 54syl6 29 . . . . . . . 8 ((a ∪ {x}) = {y} → (¬ a = x a))
5655con1d 116 . . . . . . 7 ((a ∪ {x}) = {y} → (¬ x aa = ))
5756exlimiv 1634 . . . . . 6 (y(a ∪ {x}) = {y} → (¬ x aa = ))
5857impcom 419 . . . . 5 ((¬ x a y(a ∪ {x}) = {y}) → a = )
5958gen2 1547 . . . 4 ax((¬ x a y(a ∪ {x}) = {y}) → a = )
60 elsuc 4413 . . . . . . . . 9 ((a ∪ {x}) ((n +c 1c) +c 1c) ↔ b (n +c 1c)y b(a ∪ {x}) = (b ∪ {y}))
61 vex 2862 . . . . . . . . . . . . 13 y V
6261elcompl 3225 . . . . . . . . . . . 12 (y b ↔ ¬ y b)
6362anbi2i 675 . . . . . . . . . . 11 ((b (n +c 1c) y b) ↔ (b (n +c 1c) ¬ y b))
64 simprrl 740 . . . . . . . . . . . . . . . . . . 19 ((x = y ((b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → (a ∪ {x}) = (b ∪ {y}))
65 sneq 3744 . . . . . . . . . . . . . . . . . . . 20 (x = y → {x} = {y})
6665adantr 451 . . . . . . . . . . . . . . . . . . 19 ((x = y ((b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → {x} = {y})
6764, 66difeq12d 3386 . . . . . . . . . . . . . . . . . 18 ((x = y ((b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → ((a ∪ {x}) {x}) = ((b ∪ {y}) {y}))
68 simprrr 741 . . . . . . . . . . . . . . . . . . 19 ((x = y ((b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → ¬ x a)
69 nnsucelrlem2 4425 . . . . . . . . . . . . . . . . . . 19 x a → ((a ∪ {x}) {x}) = a)
7068, 69syl 15 . . . . . . . . . . . . . . . . . 18 ((x = y ((b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → ((a ∪ {x}) {x}) = a)
71 simprlr 739 . . . . . . . . . . . . . . . . . . 19 ((x = y ((b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → ¬ y b)
72 nnsucelrlem2 4425 . . . . . . . . . . . . . . . . . . 19 y b → ((b ∪ {y}) {y}) = b)
7371, 72syl 15 . . . . . . . . . . . . . . . . . 18 ((x = y ((b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → ((b ∪ {y}) {y}) = b)
7467, 70, 733eqtr3d 2393 . . . . . . . . . . . . . . . . 17 ((x = y ((b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → a = b)
75 simprll 738 . . . . . . . . . . . . . . . . 17 ((x = y ((b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → b (n +c 1c))
7674, 75eqeltrd 2427 . . . . . . . . . . . . . . . 16 ((x = y ((b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → a (n +c 1c))
77763adantr1 1114 . . . . . . . . . . . . . . 15 ((x = y (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → a (n +c 1c))
7877ex 423 . . . . . . . . . . . . . 14 (x = y → ((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) → a (n +c 1c)))
79 simpl 443 . . . . . . . . . . . . . . . . 17 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → xy)
80 simpr3l 1016 . . . . . . . . . . . . . . . . 17 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → (a ∪ {x}) = (b ∪ {y}))
81 simpr2r 1015 . . . . . . . . . . . . . . . . 17 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → ¬ y b)
8249nnsucelrlem3 4426 . . . . . . . . . . . . . . . . 17 ((xy (a ∪ {x}) = (b ∪ {y}) ¬ y b) → b = ((a {y}) ∪ {x}))
8379, 80, 81, 82syl3anc 1182 . . . . . . . . . . . . . . . 16 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → b = ((a {y}) ∪ {x}))
84 simp22r 1075 . . . . . . . . . . . . . . . . . . 19 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → ¬ y b)
85 difsn 3845 . . . . . . . . . . . . . . . . . . . . . . . 24 y a → (a {y}) = a)
8685uneq1d 3417 . . . . . . . . . . . . . . . . . . . . . . 23 y a → ((a {y}) ∪ {x}) = (a ∪ {x}))
8786eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . 22 y a → (b = ((a {y}) ∪ {x}) ↔ b = (a ∪ {x})))
8887biimpcd 215 . . . . . . . . . . . . . . . . . . . . 21 (b = ((a {y}) ∪ {x}) → (¬ y ab = (a ∪ {x})))
89883ad2ant3 978 . . . . . . . . . . . . . . . . . . . 20 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → (¬ y ab = (a ∪ {x})))
90 simp23l 1076 . . . . . . . . . . . . . . . . . . . . . 22 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → (a ∪ {x}) = (b ∪ {y}))
9190eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → (b = (a ∪ {x}) ↔ b = (b ∪ {y})))
9261snss 3838 . . . . . . . . . . . . . . . . . . . . . . . 24 (y b ↔ {y} b)
93 ssequn2 3436 . . . . . . . . . . . . . . . . . . . . . . . 24 ({y} b ↔ (b ∪ {y}) = b)
9492, 93bitr2i 241 . . . . . . . . . . . . . . . . . . . . . . 23 ((b ∪ {y}) = by b)
9594biimpi 186 . . . . . . . . . . . . . . . . . . . . . 22 ((b ∪ {y}) = by b)
9695eqcoms 2356 . . . . . . . . . . . . . . . . . . . . 21 (b = (b ∪ {y}) → y b)
9791, 96syl6bi 219 . . . . . . . . . . . . . . . . . . . 20 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → (b = (a ∪ {x}) → y b))
9889, 97syld 40 . . . . . . . . . . . . . . . . . . 19 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → (¬ y ay b))
9984, 98mt3d 117 . . . . . . . . . . . . . . . . . 18 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → y a)
100 nnsucelrlem4 4427 . . . . . . . . . . . . . . . . . 18 (y a → ((a {y}) ∪ {y}) = a)
10199, 100syl 15 . . . . . . . . . . . . . . . . 17 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → ((a {y}) ∪ {y}) = a)
102 simpl3r 1011 . . . . . . . . . . . . . . . . . . . . 21 (((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → ¬ x a)
103 difss 3393 . . . . . . . . . . . . . . . . . . . . . 22 (a {y}) a
104103sseli 3269 . . . . . . . . . . . . . . . . . . . . 21 (x (a {y}) → x a)
105102, 104nsyl 113 . . . . . . . . . . . . . . . . . . . 20 (((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → ¬ x (a {y}))
106 simp2l 981 . . . . . . . . . . . . . . . . . . . . 21 ((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) → b (n +c 1c))
107 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . 22 (b = ((a {y}) ∪ {x}) → (b (n +c 1c) ↔ ((a {y}) ∪ {x}) (n +c 1c)))
108107biimpd 198 . . . . . . . . . . . . . . . . . . . . 21 (b = ((a {y}) ∪ {x}) → (b (n +c 1c) → ((a {y}) ∪ {x}) (n +c 1c)))
109106, 108mpan9 455 . . . . . . . . . . . . . . . . . . . 20 (((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → ((a {y}) ∪ {x}) (n +c 1c))
110 simpl1 958 . . . . . . . . . . . . . . . . . . . . 21 (((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n))
111 snex 4111 . . . . . . . . . . . . . . . . . . . . . . 23 {y} V
11212, 111difex 4107 . . . . . . . . . . . . . . . . . . . . . 22 (a {y}) V
113 eleq12 2415 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((z = x c = (a {y})) → (z cx (a {y})))
114113ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((c = (a {y}) z = x) → (z cx (a {y})))
115114notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((c = (a {y}) z = x) → (¬ z c ↔ ¬ x (a {y})))
116 sneq 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (z = x → {z} = {x})
117 uneq12 3413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((c = (a {y}) {z} = {x}) → (c ∪ {z}) = ((a {y}) ∪ {x}))
118116, 117sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((c = (a {y}) z = x) → (c ∪ {z}) = ((a {y}) ∪ {x}))
119118eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((c = (a {y}) z = x) → ((c ∪ {z}) (n +c 1c) ↔ ((a {y}) ∪ {x}) (n +c 1c)))
120115, 119anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((c = (a {y}) z = x) → ((¬ z c (c ∪ {z}) (n +c 1c)) ↔ (¬ x (a {y}) ((a {y}) ∪ {x}) (n +c 1c))))
121 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . . . 25 (c = (a {y}) → (c n ↔ (a {y}) n))
122121adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24 ((c = (a {y}) z = x) → (c n ↔ (a {y}) n))
123120, 122imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . 23 ((c = (a {y}) z = x) → (((¬ z c (c ∪ {z}) (n +c 1c)) → c n) ↔ ((¬ x (a {y}) ((a {y}) ∪ {x}) (n +c 1c)) → (a {y}) n)))
124123spc2gv 2942 . . . . . . . . . . . . . . . . . . . . . 22 (((a {y}) V x V) → (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) → ((¬ x (a {y}) ((a {y}) ∪ {x}) (n +c 1c)) → (a {y}) n)))
125112, 49, 124mp2an 653 . . . . . . . . . . . . . . . . . . . . 21 (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) → ((¬ x (a {y}) ((a {y}) ∪ {x}) (n +c 1c)) → (a {y}) n))
126110, 125syl 15 . . . . . . . . . . . . . . . . . . . 20 (((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → ((¬ x (a {y}) ((a {y}) ∪ {x}) (n +c 1c)) → (a {y}) n))
127105, 109, 126mp2and 660 . . . . . . . . . . . . . . . . . . 19 (((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → (a {y}) n)
1281273adant1 973 . . . . . . . . . . . . . . . . . 18 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → (a {y}) n)
12961snid 3760 . . . . . . . . . . . . . . . . . . . . 21 y {y}
130 eldif 3221 . . . . . . . . . . . . . . . . . . . . . 22 (y (a {y}) ↔ (y a ¬ y {y}))
131130simprbi 450 . . . . . . . . . . . . . . . . . . . . 21 (y (a {y}) → ¬ y {y})
132129, 131mt2 170 . . . . . . . . . . . . . . . . . . . 20 ¬ y (a {y})
13361elcompl 3225 . . . . . . . . . . . . . . . . . . . 20 (y ∼ (a {y}) ↔ ¬ y (a {y}))
134132, 133mpbir 200 . . . . . . . . . . . . . . . . . . 19 y ∼ (a {y})
135 eqid 2353 . . . . . . . . . . . . . . . . . . 19 ((a {y}) ∪ {y}) = ((a {y}) ∪ {y})
136 sneq 3744 . . . . . . . . . . . . . . . . . . . . . 22 (w = y → {w} = {y})
137136uneq2d 3418 . . . . . . . . . . . . . . . . . . . . 21 (w = y → ((a {y}) ∪ {w}) = ((a {y}) ∪ {y}))
138137eqeq2d 2364 . . . . . . . . . . . . . . . . . . . 20 (w = y → (((a {y}) ∪ {y}) = ((a {y}) ∪ {w}) ↔ ((a {y}) ∪ {y}) = ((a {y}) ∪ {y})))
139138rspcev 2955 . . . . . . . . . . . . . . . . . . 19 ((y ∼ (a {y}) ((a {y}) ∪ {y}) = ((a {y}) ∪ {y})) → w ∼ (a {y})((a {y}) ∪ {y}) = ((a {y}) ∪ {w}))
140134, 135, 139mp2an 653 . . . . . . . . . . . . . . . . . 18 w ∼ (a {y})((a {y}) ∪ {y}) = ((a {y}) ∪ {w})
141 compleq 3243 . . . . . . . . . . . . . . . . . . . . 21 (d = (a {y}) → ∼ d = ∼ (a {y}))
142 uneq1 3411 . . . . . . . . . . . . . . . . . . . . . 22 (d = (a {y}) → (d ∪ {w}) = ((a {y}) ∪ {w}))
143142eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 (d = (a {y}) → (((a {y}) ∪ {y}) = (d ∪ {w}) ↔ ((a {y}) ∪ {y}) = ((a {y}) ∪ {w})))
144141, 143rexeqbidv 2820 . . . . . . . . . . . . . . . . . . . 20 (d = (a {y}) → (w d((a {y}) ∪ {y}) = (d ∪ {w}) ↔ w ∼ (a {y})((a {y}) ∪ {y}) = ((a {y}) ∪ {w})))
145144rspcev 2955 . . . . . . . . . . . . . . . . . . 19 (((a {y}) n w ∼ (a {y})((a {y}) ∪ {y}) = ((a {y}) ∪ {w})) → d n w d((a {y}) ∪ {y}) = (d ∪ {w}))
146 elsuc 4413 . . . . . . . . . . . . . . . . . . 19 (((a {y}) ∪ {y}) (n +c 1c) ↔ d n w d((a {y}) ∪ {y}) = (d ∪ {w}))
147145, 146sylibr 203 . . . . . . . . . . . . . . . . . 18 (((a {y}) n w ∼ (a {y})((a {y}) ∪ {y}) = ((a {y}) ∪ {w})) → ((a {y}) ∪ {y}) (n +c 1c))
148128, 140, 147sylancl 643 . . . . . . . . . . . . . . . . 17 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → ((a {y}) ∪ {y}) (n +c 1c))
149101, 148eqeltrrd 2428 . . . . . . . . . . . . . . . 16 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) b = ((a {y}) ∪ {x})) → a (n +c 1c))
15083, 149mpd3an3 1278 . . . . . . . . . . . . . . 15 ((xy (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a))) → a (n +c 1c))
151150ex 423 . . . . . . . . . . . . . 14 (xy → ((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) → a (n +c 1c)))
15278, 151pm2.61ine 2592 . . . . . . . . . . . . 13 ((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) → a (n +c 1c))
1531523expa 1151 . . . . . . . . . . . 12 (((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b)) ((a ∪ {x}) = (b ∪ {y}) ¬ x a)) → a (n +c 1c))
154153exp32 588 . . . . . . . . . . 11 ((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) ¬ y b)) → ((a ∪ {x}) = (b ∪ {y}) → (¬ x aa (n +c 1c))))
15563, 154sylan2b 461 . . . . . . . . . 10 ((cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) (b (n +c 1c) y b)) → ((a ∪ {x}) = (b ∪ {y}) → (¬ x aa (n +c 1c))))
156155rexlimdvva 2745 . . . . . . . . 9 (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) → (b (n +c 1c)y b(a ∪ {x}) = (b ∪ {y}) → (¬ x aa (n +c 1c))))
15760, 156syl5bi 208 . . . . . . . 8 (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) → ((a ∪ {x}) ((n +c 1c) +c 1c) → (¬ x aa (n +c 1c))))
158157com23 72 . . . . . . 7 (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) → (¬ x a → ((a ∪ {x}) ((n +c 1c) +c 1c) → a (n +c 1c))))
159158imp3a 420 . . . . . 6 (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) → ((¬ x a (a ∪ {x}) ((n +c 1c) +c 1c)) → a (n +c 1c)))
160159alrimivv 1632 . . . . 5 (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) → ax((¬ x a (a ∪ {x}) ((n +c 1c) +c 1c)) → a (n +c 1c)))
161160a1i 10 . . . 4 (n Nn → (cz((¬ z c (c ∪ {z}) (n +c 1c)) → c n) → ax((¬ x a (a ∪ {x}) ((n +c 1c) +c 1c)) → a (n +c 1c))))
1621, 17, 36, 42, 48, 59, 161finds 4411 . . 3 (M Nnax((¬ x a (a ∪ {x}) (M +c 1c)) → a M))
163 nnsucelr.2 . . . . 5 X V
164 eleq1 2413 . . . . . . . 8 (x = X → (x aX a))
165164notbid 285 . . . . . . 7 (x = X → (¬ x a ↔ ¬ X a))
166 sneq 3744 . . . . . . . . 9 (x = X → {x} = {X})
167166uneq2d 3418 . . . . . . . 8 (x = X → (a ∪ {x}) = (a ∪ {X}))
168167eleq1d 2419 . . . . . . 7 (x = X → ((a ∪ {x}) (M +c 1c) ↔ (a ∪ {X}) (M +c 1c)))
169165, 168anbi12d 691 . . . . . 6 (x = X → ((¬ x a (a ∪ {x}) (M +c 1c)) ↔ (¬ X a (a ∪ {X}) (M +c 1c))))
170169imbi1d 308 . . . . 5 (x = X → (((¬ x a (a ∪ {x}) (M +c 1c)) → a M) ↔ ((¬ X a (a ∪ {X}) (M +c 1c)) → a M)))
171163, 170spcv 2945 . . . 4 (x((¬ x a (a ∪ {x}) (M +c 1c)) → a M) → ((¬ X a (a ∪ {X}) (M +c 1c)) → a M))
172171alimi 1559 . . 3 (ax((¬ x a (a ∪ {x}) (M +c 1c)) → a M) → a((¬ X a (a ∪ {X}) (M +c 1c)) → a M))
173 nnsucelr.1 . . . 4 A V
174 eleq2 2414 . . . . . . 7 (a = A → (X aX A))
175174notbid 285 . . . . . 6 (a = A → (¬ X a ↔ ¬ X A))
176 uneq1 3411 . . . . . . 7 (a = A → (a ∪ {X}) = (A ∪ {X}))
177176eleq1d 2419 . . . . . 6 (a = A → ((a ∪ {X}) (M +c 1c) ↔ (A ∪ {X}) (M +c 1c)))
178175, 177anbi12d 691 . . . . 5 (a = A → ((¬ X a (a ∪ {X}) (M +c 1c)) ↔ (¬ X A (A ∪ {X}) (M +c 1c))))
179 eleq1 2413 . . . . 5 (a = A → (a MA M))
180178, 179imbi12d 311 . . . 4 (a = A → (((¬ X a (a ∪ {X}) (M +c 1c)) → a M) ↔ ((¬ X A (A ∪ {X}) (M +c 1c)) → A M)))
181173, 180spcv 2945 . . 3 (a((¬ X a (a ∪ {X}) (M +c 1c)) → a M) → ((¬ X A (A ∪ {X}) (M +c 1c)) → A M))
182162, 172, 1813syl 18 . 2 (M Nn → ((¬ X A (A ∪ {X}) (M +c 1c)) → A M))
183182imp 418 1 ((M Nn X A (A ∪ {X}) (M +c 1c))) → A M)
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  wne 2516  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cun 3207   wss 3257  c0 3550  {csn 3737  1cc1c 4134   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-idk 4195  df-0c 4377  df-addc 4378  df-nnc 4379
This theorem is referenced by:  nndisjeq  4429  prepeano4  4451  ssfin  4470
  Copyright terms: Public domain W3C validator