Step | Hyp | Ref
| Expression |
1 | | n0 3559 |
. . 3
⊢ ((M +c 1c) ≠
∅ ↔ ∃a a ∈ (M +c
1c)) |
2 | | elsuc 4413 |
. . . . 5
⊢ (a ∈ (M +c 1c) ↔
∃b ∈ M ∃x ∈ ∼ ba = (b ∪ {x})) |
3 | | simplll 734 |
. . . . . . . 8
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → M
∈ Nn
) |
4 | | simpllr 735 |
. . . . . . . 8
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → N
∈ Nn
) |
5 | | simprl 732 |
. . . . . . . 8
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → b
∈ M) |
6 | | simprr 733 |
. . . . . . . . . 10
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → x
∈ ∼ b) |
7 | | vex 2862 |
. . . . . . . . . . 11
⊢ x ∈
V |
8 | 7 | elcompl 3225 |
. . . . . . . . . 10
⊢ (x ∈ ∼ b ↔ ¬ x
∈ b) |
9 | 6, 8 | sylib 188 |
. . . . . . . . 9
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → ¬ x ∈ b) |
10 | 7 | elsuci 4414 |
. . . . . . . . . . . 12
⊢ ((b ∈ M ∧ ¬ x ∈ b) → (b
∪ {x}) ∈ (M
+c 1c)) |
11 | 8, 10 | sylan2b 461 |
. . . . . . . . . . 11
⊢ ((b ∈ M ∧ x ∈ ∼ b) → (b
∪ {x}) ∈ (M
+c 1c)) |
12 | 11 | adantl 452 |
. . . . . . . . . 10
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → (b
∪ {x}) ∈ (M
+c 1c)) |
13 | | simplr 731 |
. . . . . . . . . 10
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → (M
+c 1c) = (N +c
1c)) |
14 | 12, 13 | eleqtrd 2429 |
. . . . . . . . 9
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → (b
∪ {x}) ∈ (N
+c 1c)) |
15 | | vex 2862 |
. . . . . . . . . 10
⊢ b ∈
V |
16 | 15, 7 | nnsucelr 4428 |
. . . . . . . . 9
⊢ ((N ∈ Nn ∧ (¬ x ∈ b ∧ (b ∪ {x})
∈ (N
+c 1c))) → b ∈ N) |
17 | 4, 9, 14, 16 | syl12anc 1180 |
. . . . . . . 8
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → b
∈ N) |
18 | | nnceleq 4430 |
. . . . . . . 8
⊢ (((M ∈ Nn ∧ N ∈ Nn ) ∧ (b ∈ M ∧ b ∈ N)) → M =
N) |
19 | 3, 4, 5, 17, 18 | syl22anc 1183 |
. . . . . . 7
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → M =
N) |
20 | 19 | a1d 22 |
. . . . . 6
⊢ ((((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) ∧ (b ∈ M ∧ x ∈ ∼ b)) → (a =
(b ∪ {x}) → M =
N)) |
21 | 20 | rexlimdvva 2745 |
. . . . 5
⊢ (((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) → (∃b ∈ M ∃x ∈ ∼ ba = (b ∪ {x})
→ M = N)) |
22 | 2, 21 | syl5bi 208 |
. . . 4
⊢ (((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) → (a ∈ (M
+c 1c) → M = N)) |
23 | 22 | exlimdv 1636 |
. . 3
⊢ (((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) → (∃a a ∈ (M
+c 1c) → M = N)) |
24 | 1, 23 | syl5bi 208 |
. 2
⊢ (((M ∈ Nn ∧ N ∈ Nn ) ∧ (M +c 1c) =
(N +c
1c)) → ((M
+c 1c) ≠ ∅ → M =
N)) |
25 | 24 | impr 602 |
1
⊢ (((M ∈ Nn ∧ N ∈ Nn ) ∧ ((M +c 1c) =
(N +c
1c) ∧ (M +c 1c) ≠
∅)) → M = N) |