Step | Hyp | Ref
| Expression |
1 | | nnsucelrlem1 4424 |
. . . 4
⊢ {m ∣ ∀a∀x((¬
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 |
4 | 2, 3 | syl6eq 2401 |
. . . . . . . . 9
⊢ (m = 0c → (m +c 1c) =
1c) |
5 | 4 | eleq2d 2420 |
. . . . . . . 8
⊢ (m = 0c → ((a ∪ {x})
∈ (m
+c 1c) ↔ (a ∪ {x})
∈ 1c)) |
6 | | el1c 4139 |
. . . . . . . 8
⊢ ((a ∪ {x})
∈ 1c ↔ ∃y(a ∪ {x}) =
{y}) |
7 | 5, 6 | syl6bb 252 |
. . . . . . 7
⊢ (m = 0c → ((a ∪ {x})
∈ (m
+c 1c) ↔ ∃y(a ∪ {x}) =
{y})) |
8 | 7 | anbi2d 684 |
. . . . . 6
⊢ (m = 0c → ((¬ x ∈ a ∧ (a ∪ {x})
∈ (m
+c 1c)) ↔ (¬ x ∈ a ∧ ∃y(a ∪ {x}) =
{y}))) |
9 | | eleq2 2414 |
. . . . . . 7
⊢ (m = 0c → (a ∈ m ↔ a ∈ 0c)) |
10 | | df-0c 4377 |
. . . . . . . . 9
⊢
0c = {∅} |
11 | 10 | eleq2i 2417 |
. . . . . . . 8
⊢ (a ∈
0c ↔ a ∈ {∅}) |
12 | | vex 2862 |
. . . . . . . . 9
⊢ a ∈
V |
13 | 12 | elsnc 3756 |
. . . . . . . 8
⊢ (a ∈ {∅} ↔ a =
∅) |
14 | 11, 13 | bitri 240 |
. . . . . . 7
⊢ (a ∈
0c ↔ a = ∅) |
15 | 9, 14 | syl6bb 252 |
. . . . . 6
⊢ (m = 0c → (a ∈ m ↔ a =
∅)) |
16 | 8, 15 | imbi12d 311 |
. . . . 5
⊢ (m = 0c → (((¬ x ∈ a ∧ (a ∪ {x})
∈ (m
+c 1c)) → a ∈ m) ↔ ((¬ x ∈ a ∧ ∃y(a ∪ {x}) =
{y}) → a = ∅))) |
17 | 16 | 2albidv 1627 |
. . . 4
⊢ (m = 0c → (∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (m +c 1c)) →
a ∈
m) ↔ ∀a∀x((¬
x ∈
a ∧ ∃y(a ∪ {x}) =
{y}) → a = ∅))) |
18 | | addceq1 4383 |
. . . . . . . . 9
⊢ (m = n →
(m +c
1c) = (n
+c 1c)) |
19 | 18 | eleq2d 2420 |
. . . . . . . 8
⊢ (m = n →
((a ∪ {x}) ∈ (m +c 1c) ↔
(a ∪ {x}) ∈ (n +c
1c))) |
20 | 19 | anbi2d 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 ∈
m ↔ a ∈ n)) |
22 | 20, 21 | imbi12d 311 |
. . . . . 6
⊢ (m = n →
(((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m) ↔
((¬ x ∈ a ∧ (a ∪
{x}) ∈
(n +c
1c)) → a ∈ n))) |
23 | 22 | 2albidv 1627 |
. . . . 5
⊢ (m = n →
(∀a∀x((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m) ↔
∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (n +c 1c)) →
a ∈
n))) |
24 | | eleq12 2415 |
. . . . . . . . . 10
⊢ ((x = z ∧ a = c) → (x
∈ a
↔ z ∈ c)) |
25 | 24 | ancoms 439 |
. . . . . . . . 9
⊢ ((a = c ∧ x = z) → (x
∈ a
↔ z ∈ c)) |
26 | 25 | notbid 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})) |
29 | 27, 28 | sylan2 460 |
. . . . . . . . 9
⊢ ((a = c ∧ x = z) → (a
∪ {x}) = (c ∪ {z})) |
30 | 29 | eleq1d 2419 |
. . . . . . . 8
⊢ ((a = c ∧ x = z) → ((a
∪ {x}) ∈ (n
+c 1c) ↔ (c ∪ {z})
∈ (n
+c 1c))) |
31 | 26, 30 | anbi12d 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 ∈
n ↔ c ∈ n)) |
33 | 32 | adantr 451 |
. . . . . . 7
⊢ ((a = c ∧ x = z) → (a
∈ n
↔ c ∈ n)) |
34 | 31, 33 | imbi12d 311 |
. . . . . 6
⊢ ((a = c ∧ x = z) → (((¬ x ∈ a ∧ (a ∪ {x})
∈ (n
+c 1c)) → a ∈ n) ↔ ((¬ z ∈ c ∧ (c ∪ {z})
∈ (n
+c 1c)) → c ∈ n))) |
35 | 34 | cbval2v 2006 |
. . . . 5
⊢ (∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (n +c 1c)) →
a ∈
n) ↔ ∀c∀z((¬
z ∈
c ∧
(c ∪ {z}) ∈ (n +c 1c)) →
c ∈
n)) |
36 | 23, 35 | syl6bb 252 |
. . . 4
⊢ (m = n →
(∀a∀x((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m) ↔
∀c∀z((¬
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)) |
38 | 37 | eleq2d 2420 |
. . . . . . 7
⊢ (m = (n
+c 1c) → ((a ∪ {x})
∈ (m
+c 1c) ↔ (a ∪ {x})
∈ ((n
+c 1c) +c
1c))) |
39 | 38 | anbi2d 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 ∈ m ↔ a ∈ (n
+c 1c))) |
41 | 39, 40 | imbi12d 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)))) |
42 | 41 | 2albidv 1627 |
. . . 4
⊢ (m = (n
+c 1c) → (∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (m +c 1c)) →
a ∈
m) ↔ ∀a∀x((¬
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)) |
44 | 43 | eleq2d 2420 |
. . . . . . 7
⊢ (m = M →
((a ∪ {x}) ∈ (m +c 1c) ↔
(a ∪ {x}) ∈ (M +c
1c))) |
45 | 44 | anbi2d 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 ∈
m ↔ a ∈ M)) |
47 | 45, 46 | imbi12d 311 |
. . . . 5
⊢ (m = M →
(((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m) ↔
((¬ x ∈ a ∧ (a ∪
{x}) ∈
(M +c
1c)) → a ∈ M))) |
48 | 47 | 2albidv 1627 |
. . . 4
⊢ (m = M →
(∀a∀x((¬ x ∈ a ∧ (a ∪
{x}) ∈
(m +c
1c)) → a ∈ m) ↔
∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (M +c 1c)) →
a ∈
M))) |
49 | | vex 2862 |
. . . . . . . . . . 11
⊢ x ∈
V |
50 | 49 | unsneqsn 3887 |
. . . . . . . . . 10
⊢ ((a ∪ {x}) =
{y} → (a = ∅ ∨ a = {x})) |
51 | 50 | ord 366 |
. . . . . . . . 9
⊢ ((a ∪ {x}) =
{y} → (¬ a = ∅ →
a = {x})) |
52 | 49 | snid 3760 |
. . . . . . . . . 10
⊢ x ∈ {x} |
53 | | eleq2 2414 |
. . . . . . . . . 10
⊢ (a = {x} →
(x ∈
a ↔ x ∈ {x})) |
54 | 52, 53 | mpbiri 224 |
. . . . . . . . 9
⊢ (a = {x} →
x ∈
a) |
55 | 51, 54 | syl6 29 |
. . . . . . . 8
⊢ ((a ∪ {x}) =
{y} → (¬ a = ∅ →
x ∈
a)) |
56 | 55 | con1d 116 |
. . . . . . 7
⊢ ((a ∪ {x}) =
{y} → (¬ x ∈ a → a =
∅)) |
57 | 56 | exlimiv 1634 |
. . . . . 6
⊢ (∃y(a ∪ {x}) =
{y} → (¬ x ∈ a → a =
∅)) |
58 | 57 | impcom 419 |
. . . . 5
⊢ ((¬ x ∈ a ∧ ∃y(a ∪ {x}) =
{y}) → a = ∅) |
59 | 58 | gen2 1547 |
. . . 4
⊢ ∀a∀x((¬
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 |
62 | 61 | elcompl 3225 |
. . . . . . . . . . . 12
⊢ (y ∈ ∼ b ↔ ¬ y
∈ b) |
63 | 62 | anbi2i 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}) |
66 | 65 | adantr 451 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((x = y ∧ ((b ∈ (n
+c 1c) ∧
¬ y ∈
b) ∧
((a ∪ {x}) = (b ∪
{y}) ∧
¬ x ∈
a))) → {x} = {y}) |
67 | 64, 66 | difeq12d 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) |
70 | 68, 69 | syl 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) |
73 | 71, 72 | syl 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((x = y ∧ ((b ∈ (n
+c 1c) ∧
¬ y ∈
b) ∧
((a ∪ {x}) = (b ∪
{y}) ∧
¬ x ∈
a))) → ((b ∪ {y})
∖ {y}) =
b) |
74 | 67, 70, 73 | 3eqtr3d 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)) |
76 | 74, 75 | eqeltrd 2427 |
. . . . . . . . . . . . . . . 16
⊢ ((x = y ∧ ((b ∈ (n
+c 1c) ∧
¬ y ∈
b) ∧
((a ∪ {x}) = (b ∪
{y}) ∧
¬ x ∈
a))) → a ∈ (n +c
1c)) |
77 | 76 | 3adantr1 1114 |
. . . . . . . . . . . . . . 15
⊢ ((x = y ∧ (∀c∀z((¬ 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)) |
78 | 77 | ex 423 |
. . . . . . . . . . . . . 14
⊢ (x = y →
((∀c∀z((¬ 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
⊢ ((x ≠ y ∧ (∀c∀z((¬ z ∈ c ∧ (c ∪
{z}) ∈
(n +c
1c)) → c ∈ n) ∧ (b ∈ (n
+c 1c) ∧
¬ y ∈
b) ∧
((a ∪ {x}) = (b ∪
{y}) ∧
¬ x ∈
a))) → x ≠ y) |
80 | | simpr3l 1016 |
. . . . . . . . . . . . . . . . 17
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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
⊢ ((x ≠ y ∧ (∀c∀z((¬ z ∈ c ∧ (c ∪
{z}) ∈
(n +c
1c)) → c ∈ n) ∧ (b ∈ (n
+c 1c) ∧
¬ y ∈
b) ∧
((a ∪ {x}) = (b ∪
{y}) ∧
¬ x ∈
a))) → ¬ y ∈ b) |
82 | 49 | nnsucelrlem3 4426 |
. . . . . . . . . . . . . . . . 17
⊢ ((x ≠ y ∧ (a ∪
{x}) = (b ∪ {y})
∧ ¬ y
∈ b)
→ b = ((a ∖ {y}) ∪ {x})) |
83 | 79, 80, 81, 82 | syl3anc 1182 |
. . . . . . . . . . . . . . . 16
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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) |
86 | 85 | uneq1d 3417 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬ y ∈ a → ((a
∖ {y})
∪ {x}) = (a ∪ {x})) |
87 | 86 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬ y ∈ a → (b =
((a ∖
{y}) ∪ {x}) ↔ b =
(a ∪ {x}))) |
88 | 87 | biimpcd 215 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (b = ((a ∖ {y}) ∪
{x}) → (¬ y ∈ a → b =
(a ∪ {x}))) |
89 | 88 | 3ad2ant3 978 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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 → b =
(a ∪ {x}))) |
90 | | simp23l 1076 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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})) |
91 | 90 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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}))) |
92 | 61 | snss 3838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (y ∈ b ↔ {y}
⊆ b) |
93 | | ssequn2 3436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ({y} ⊆ b ↔ (b
∪ {y}) = b) |
94 | 92, 93 | bitr2i 241 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((b ∪ {y}) =
b ↔ y ∈ b) |
95 | 94 | biimpi 186 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((b ∪ {y}) =
b → y ∈ b) |
96 | 95 | eqcoms 2356 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (b = (b ∪
{y}) → y ∈ b) |
97 | 91, 96 | syl6bi 219 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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)) |
98 | 89, 97 | syld 40 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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 → y ∈ b)) |
99 | 84, 98 | mt3d 117 |
. . . . . . . . . . . . . . . . . 18
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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) |
101 | 99, 100 | syl 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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
⊢ (((∀c∀z((¬
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 |
104 | 103 | sseli 3269 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (x ∈ (a ∖ {y}) → x
∈ a) |
105 | 102, 104 | nsyl 113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((∀c∀z((¬
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
⊢ ((∀c∀z((¬
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))) |
108 | 107 | biimpd 198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (b = ((a ∖ {y}) ∪
{x}) → (b ∈ (n +c 1c) →
((a ∖
{y}) ∪ {x}) ∈ (n +c
1c))) |
109 | 106, 108 | mpan9 455 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((∀c∀z((¬
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
⊢ (((∀c∀z((¬
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})) → ∀c∀z((¬
z ∈
c ∧
(c ∪ {z}) ∈ (n +c 1c)) →
c ∈
n)) |
111 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {y} ∈
V |
112 | 12, 111 | difex 4107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (a ∖ {y}) ∈
V |
113 | | eleq12 2415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((z = x ∧ c = (a ∖ {y})) → (z
∈ c
↔ x ∈ (a ∖ {y}))) |
114 | 113 | ancoms 439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((c = (a ∖ {y}) ∧ z = x) → (z
∈ c
↔ x ∈ (a ∖ {y}))) |
115 | 114 | notbid 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})) |
118 | 116, 117 | sylan2 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((c = (a ∖ {y}) ∧ z = x) → (c
∪ {z}) = ((a ∖ {y}) ∪ {x})) |
119 | 118 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((c = (a ∖ {y}) ∧ z = x) → ((c
∪ {z}) ∈ (n
+c 1c) ↔ ((a ∖ {y}) ∪ {x})
∈ (n
+c 1c))) |
120 | 115, 119 | anbi12d 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)) |
122 | 121 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((c = (a ∖ {y}) ∧ z = x) → (c
∈ n
↔ (a ∖ {y}) ∈ n)) |
123 | 120, 122 | imbi12d 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))) |
124 | 123 | spc2gv 2942 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((a ∖ {y}) ∈ V ∧ x ∈ V) → (∀c∀z((¬
z ∈
c ∧
(c ∪ {z}) ∈ (n +c 1c)) →
c ∈
n) → ((¬ x ∈ (a ∖ {y}) ∧ ((a ∖ {y}) ∪ {x})
∈ (n
+c 1c)) → (a ∖ {y}) ∈ n))) |
125 | 112, 49, 124 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∀c∀z((¬
z ∈
c ∧
(c ∪ {z}) ∈ (n +c 1c)) →
c ∈
n) → ((¬ x ∈ (a ∖ {y}) ∧ ((a ∖ {y}) ∪ {x})
∈ (n
+c 1c)) → (a ∖ {y}) ∈ n)) |
126 | 110, 125 | syl 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((∀c∀z((¬
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)) |
127 | 105, 109,
126 | mp2and 660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((∀c∀z((¬
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) |
128 | 127 | 3adant1 973 |
. . . . . . . . . . . . . . . . . 18
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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) |
129 | 61 | snid 3760 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ y ∈ {y} |
130 | | eldif 3221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (y ∈ (a ∖ {y}) ↔ (y
∈ a ∧ ¬ y ∈ {y})) |
131 | 130 | simprbi 450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (y ∈ (a ∖ {y}) → ¬ y ∈ {y}) |
132 | 129, 131 | mt2 170 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ¬ y ∈ (a ∖ {y}) |
133 | 61 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (y ∈ ∼
(a ∖
{y}) ↔ ¬ y ∈ (a ∖ {y})) |
134 | 132, 133 | mpbir 200 |
. . . . . . . . . . . . . . . . . . 19
⊢ y ∈ ∼
(a ∖
{y}) |
135 | | eqid 2353 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((a ∖ {y}) ∪ {y}) =
((a ∖
{y}) ∪ {y}) |
136 | | sneq 3744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (w = y →
{w} = {y}) |
137 | 136 | uneq2d 3418 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (w = y →
((a ∖
{y}) ∪ {w}) = ((a ∖ {y}) ∪
{y})) |
138 | 137 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (w = y →
(((a ∖
{y}) ∪ {y}) = ((a ∖ {y}) ∪
{w}) ↔ ((a ∖ {y}) ∪ {y}) =
((a ∖
{y}) ∪ {y}))) |
139 | 138 | rspcev 2955 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((y ∈ ∼
(a ∖
{y}) ∧
((a ∖
{y}) ∪ {y}) = ((a ∖ {y}) ∪
{y})) → ∃w ∈ ∼ (a
∖ {y})((a ∖ {y}) ∪
{y}) = ((a ∖ {y}) ∪ {w})) |
140 | 134, 135,
139 | mp2an 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})) |
143 | 142 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (d = (a ∖ {y}) →
(((a ∖
{y}) ∪ {y}) = (d ∪
{w}) ↔ ((a ∖ {y}) ∪ {y}) =
((a ∖
{y}) ∪ {w}))) |
144 | 141, 143 | rexeqbidv 2820 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (d = (a ∖ {y}) →
(∃w
∈ ∼ d((a ∖ {y}) ∪
{y}) = (d ∪ {w})
↔ ∃w ∈ ∼
(a ∖
{y})((a
∖ {y})
∪ {y}) = ((a ∖ {y}) ∪ {w}))) |
145 | 144 | rspcev 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})) |
147 | 145, 146 | sylibr 203 |
. . . . . . . . . . . . . . . . . 18
⊢ (((a ∖ {y}) ∈ n ∧ ∃w ∈ ∼ (a
∖ {y})((a ∖ {y}) ∪
{y}) = ((a ∖ {y}) ∪ {w}))
→ ((a ∖ {y}) ∪
{y}) ∈
(n +c
1c)) |
148 | 128, 140,
147 | sylancl 643 |
. . . . . . . . . . . . . . . . 17
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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)) |
149 | 101, 148 | eqeltrrd 2428 |
. . . . . . . . . . . . . . . 16
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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)) |
150 | 83, 149 | mpd3an3 1278 |
. . . . . . . . . . . . . . 15
⊢ ((x ≠ y ∧ (∀c∀z((¬ 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)) |
151 | 150 | ex 423 |
. . . . . . . . . . . . . 14
⊢ (x ≠ y →
((∀c∀z((¬ 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))) |
152 | 78, 151 | pm2.61ine 2592 |
. . . . . . . . . . . . 13
⊢ ((∀c∀z((¬
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)) |
153 | 152 | 3expa 1151 |
. . . . . . . . . . . 12
⊢ (((∀c∀z((¬
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)) |
154 | 153 | exp32 588 |
. . . . . . . . . . 11
⊢ ((∀c∀z((¬
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)))) |
155 | 63, 154 | sylan2b 461 |
. . . . . . . . . 10
⊢ ((∀c∀z((¬
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)))) |
156 | 155 | rexlimdvva 2745 |
. . . . . . . . 9
⊢ (∀c∀z((¬
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)))) |
157 | 60, 156 | syl5bi 208 |
. . . . . . . 8
⊢ (∀c∀z((¬
z ∈
c ∧
(c ∪ {z}) ∈ (n +c 1c)) →
c ∈
n) → ((a ∪ {x})
∈ ((n
+c 1c) +c
1c) → (¬ x ∈ a →
a ∈
(n +c
1c)))) |
158 | 157 | com23 72 |
. . . . . . 7
⊢ (∀c∀z((¬
z ∈
c ∧
(c ∪ {z}) ∈ (n +c 1c)) →
c ∈
n) → (¬ x ∈ a → ((a
∪ {x}) ∈ ((n
+c 1c) +c
1c) → a ∈ (n
+c 1c)))) |
159 | 158 | imp3a 420 |
. . . . . 6
⊢ (∀c∀z((¬
z ∈
c ∧
(c ∪ {z}) ∈ (n +c 1c)) →
c ∈
n) → ((¬ x ∈ a ∧ (a ∪ {x})
∈ ((n
+c 1c) +c
1c)) → a ∈ (n
+c 1c))) |
160 | 159 | alrimivv 1632 |
. . . . 5
⊢ (∀c∀z((¬
z ∈
c ∧
(c ∪ {z}) ∈ (n +c 1c)) →
c ∈
n) → ∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ ((n +c 1c)
+c 1c)) → a ∈ (n +c
1c))) |
161 | 160 | a1i 10 |
. . . 4
⊢ (n ∈ Nn → (∀c∀z((¬ z ∈ c ∧ (c ∪
{z}) ∈
(n +c
1c)) → c ∈ n) →
∀a∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ ((n +c 1c)
+c 1c)) → a ∈ (n +c
1c)))) |
162 | 1, 17, 36, 42, 48, 59, 161 | finds 4411 |
. . 3
⊢ (M ∈ Nn → ∀a∀x((¬ x ∈ a ∧ (a ∪
{x}) ∈
(M +c
1c)) → a ∈ M)) |
163 | | nnsucelr.2 |
. . . . 5
⊢ X ∈
V |
164 | | eleq1 2413 |
. . . . . . . 8
⊢ (x = X →
(x ∈
a ↔ X ∈ a)) |
165 | 164 | notbid 285 |
. . . . . . 7
⊢ (x = X →
(¬ x ∈ a ↔
¬ X ∈
a)) |
166 | | sneq 3744 |
. . . . . . . . 9
⊢ (x = X →
{x} = {X}) |
167 | 166 | uneq2d 3418 |
. . . . . . . 8
⊢ (x = X →
(a ∪ {x}) = (a ∪
{X})) |
168 | 167 | eleq1d 2419 |
. . . . . . 7
⊢ (x = X →
((a ∪ {x}) ∈ (M +c 1c) ↔
(a ∪ {X}) ∈ (M +c
1c))) |
169 | 165, 168 | anbi12d 691 |
. . . . . 6
⊢ (x = X →
((¬ x ∈ a ∧ (a ∪
{x}) ∈
(M +c
1c)) ↔ (¬ X
∈ a ∧ (a ∪
{X}) ∈
(M +c
1c)))) |
170 | 169 | imbi1d 308 |
. . . . 5
⊢ (x = X →
(((¬ x ∈ a ∧ (a ∪
{x}) ∈
(M +c
1c)) → a ∈ M) ↔
((¬ X ∈ a ∧ (a ∪
{X}) ∈
(M +c
1c)) → a ∈ M))) |
171 | 163, 170 | spcv 2945 |
. . . 4
⊢ (∀x((¬
x ∈
a ∧
(a ∪ {x}) ∈ (M +c 1c)) →
a ∈
M) → ((¬ X ∈ a ∧ (a ∪ {X})
∈ (M
+c 1c)) → a ∈ M)) |
172 | 171 | alimi 1559 |
. . 3
⊢ (∀a∀x((¬
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 ∈
a ↔ X ∈ A)) |
175 | 174 | notbid 285 |
. . . . . 6
⊢ (a = A →
(¬ X ∈ a ↔
¬ X ∈
A)) |
176 | | uneq1 3411 |
. . . . . . 7
⊢ (a = A →
(a ∪ {X}) = (A ∪
{X})) |
177 | 176 | eleq1d 2419 |
. . . . . 6
⊢ (a = A →
((a ∪ {X}) ∈ (M +c 1c) ↔
(A ∪ {X}) ∈ (M +c
1c))) |
178 | 175, 177 | anbi12d 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 ∈
M ↔ A ∈ M)) |
180 | 178, 179 | imbi12d 311 |
. . . 4
⊢ (a = A →
(((¬ X ∈ a ∧ (a ∪
{X}) ∈
(M +c
1c)) → a ∈ M) ↔
((¬ X ∈ A ∧ (A ∪
{X}) ∈
(M +c
1c)) → A ∈ M))) |
181 | 173, 180 | spcv 2945 |
. . 3
⊢ (∀a((¬
X ∈
a ∧
(a ∪ {X}) ∈ (M +c 1c)) →
a ∈
M) → ((¬ X ∈ A ∧ (A ∪ {X})
∈ (M
+c 1c)) → A ∈ M)) |
182 | 162, 172,
181 | 3syl 18 |
. 2
⊢ (M ∈ Nn → ((¬ X
∈ A ∧ (A ∪
{X}) ∈
(M +c
1c)) → A ∈ M)) |
183 | 182 | imp 418 |
1
⊢ ((M ∈ Nn ∧ (¬ X ∈ A ∧ (A ∪ {X})
∈ (M
+c 1c))) → A ∈ M) |