Step | Hyp | Ref
| Expression |
1 | | n0 3559 |
. . 3
⊢ ((A +c 1c) ≠
∅ ↔ ∃a a ∈ (A +c
1c)) |
2 | | peano2 4403 |
. . . . . . . 8
⊢ (A ∈ Nn → (A
+c 1c) ∈
Nn ) |
3 | | tfincl 4492 |
. . . . . . . 8
⊢ ((A +c 1c) ∈ Nn → Tfin (A
+c 1c) ∈
Nn ) |
4 | 2, 3 | syl 15 |
. . . . . . 7
⊢ (A ∈ Nn → Tfin
(A +c
1c) ∈ Nn ) |
5 | 4 | adantr 451 |
. . . . . 6
⊢ ((A ∈ Nn ∧ a ∈ (A +c 1c)) →
Tfin (A +c 1c) ∈ Nn
) |
6 | | tfincl 4492 |
. . . . . . . 8
⊢ (A ∈ Nn → Tfin
A ∈ Nn ) |
7 | | peano2 4403 |
. . . . . . . 8
⊢ ( Tfin A
∈ Nn → (
Tfin A +c 1c) ∈ Nn
) |
8 | 6, 7 | syl 15 |
. . . . . . 7
⊢ (A ∈ Nn → ( Tfin
A +c
1c) ∈ Nn ) |
9 | 8 | adantr 451 |
. . . . . 6
⊢ ((A ∈ Nn ∧ a ∈ (A +c 1c)) →
( Tfin A +c 1c) ∈ Nn
) |
10 | | tfinpw1 4494 |
. . . . . . 7
⊢ (((A +c 1c) ∈ Nn ∧ a ∈ (A
+c 1c)) → ℘1a ∈ Tfin (A
+c 1c)) |
11 | 2, 10 | sylan 457 |
. . . . . 6
⊢ ((A ∈ Nn ∧ a ∈ (A +c 1c)) →
℘1a ∈ Tfin (A
+c 1c)) |
12 | | elsuc 4413 |
. . . . . . . 8
⊢ (a ∈ (A +c 1c) ↔
∃b ∈ A ∃x ∈ ∼ ba = (b ∪ {x})) |
13 | | tfinpw1 4494 |
. . . . . . . . . . . 12
⊢ ((A ∈ Nn ∧ b ∈ A) → ℘1b ∈ Tfin A) |
14 | 13 | adantrr 697 |
. . . . . . . . . . 11
⊢ ((A ∈ Nn ∧ (b ∈ A ∧ x ∈ ∼ b)) → ℘1b ∈ Tfin A) |
15 | | vex 2862 |
. . . . . . . . . . . . . . 15
⊢ x ∈
V |
16 | 15 | elcompl 3225 |
. . . . . . . . . . . . . 14
⊢ (x ∈ ∼ b ↔ ¬ x
∈ b) |
17 | | snelpw1 4146 |
. . . . . . . . . . . . . 14
⊢ ({x} ∈ ℘1b ↔ x ∈ b) |
18 | 16, 17 | xchbinxr 302 |
. . . . . . . . . . . . 13
⊢ (x ∈ ∼ b ↔ ¬ {x} ∈ ℘1b) |
19 | 18 | biimpi 186 |
. . . . . . . . . . . 12
⊢ (x ∈ ∼ b → ¬ {x} ∈ ℘1b) |
20 | 19 | ad2antll 709 |
. . . . . . . . . . 11
⊢ ((A ∈ Nn ∧ (b ∈ A ∧ x ∈ ∼ b)) → ¬ {x} ∈ ℘1b) |
21 | | snex 4111 |
. . . . . . . . . . . 12
⊢ {x} ∈
V |
22 | 21 | elsuci 4414 |
. . . . . . . . . . 11
⊢ ((℘1b ∈ Tfin A
∧ ¬ {x} ∈ ℘1b) → (℘1b ∪ {{x}})
∈ ( Tfin A
+c 1c)) |
23 | 14, 20, 22 | syl2anc 642 |
. . . . . . . . . 10
⊢ ((A ∈ Nn ∧ (b ∈ A ∧ x ∈ ∼ b)) → (℘1b ∪ {{x}})
∈ ( Tfin A
+c 1c)) |
24 | | pw1eq 4143 |
. . . . . . . . . . . 12
⊢ (a = (b ∪
{x}) → ℘1a = ℘1(b ∪ {x})) |
25 | | pw1un 4163 |
. . . . . . . . . . . . 13
⊢ ℘1(b ∪ {x}) =
(℘1b ∪ ℘1{x}) |
26 | 15 | pw1sn 4165 |
. . . . . . . . . . . . . 14
⊢ ℘1{x} = {{x}} |
27 | 26 | uneq2i 3415 |
. . . . . . . . . . . . 13
⊢ (℘1b ∪ ℘1{x}) = (℘1b ∪ {{x}}) |
28 | 25, 27 | eqtri 2373 |
. . . . . . . . . . . 12
⊢ ℘1(b ∪ {x}) =
(℘1b ∪ {{x}}) |
29 | 24, 28 | syl6eq 2401 |
. . . . . . . . . . 11
⊢ (a = (b ∪
{x}) → ℘1a = (℘1b ∪ {{x}})) |
30 | 29 | eleq1d 2419 |
. . . . . . . . . 10
⊢ (a = (b ∪
{x}) → (℘1a ∈ ( Tfin A
+c 1c) ↔ (℘1b ∪ {{x}})
∈ ( Tfin A
+c 1c))) |
31 | 23, 30 | syl5ibrcom 213 |
. . . . . . . . 9
⊢ ((A ∈ Nn ∧ (b ∈ A ∧ x ∈ ∼ b)) → (a =
(b ∪ {x}) → ℘1a ∈ ( Tfin A
+c 1c))) |
32 | 31 | rexlimdvva 2745 |
. . . . . . . 8
⊢ (A ∈ Nn → (∃b ∈ A ∃x ∈ ∼ ba = (b ∪ {x})
→ ℘1a ∈ ( Tfin A
+c 1c))) |
33 | 12, 32 | syl5bi 208 |
. . . . . . 7
⊢ (A ∈ Nn → (a ∈ (A
+c 1c) → ℘1a ∈ ( Tfin A
+c 1c))) |
34 | 33 | imp 418 |
. . . . . 6
⊢ ((A ∈ Nn ∧ a ∈ (A +c 1c)) →
℘1a ∈ ( Tfin A
+c 1c)) |
35 | | nnceleq 4430 |
. . . . . 6
⊢ ((( Tfin (A
+c 1c) ∈
Nn ∧ ( Tfin A
+c 1c) ∈
Nn ) ∧ (℘1a ∈ Tfin (A
+c 1c) ∧
℘1a ∈ ( Tfin A
+c 1c))) → Tfin (A
+c 1c) = ( Tfin A
+c 1c)) |
36 | 5, 9, 11, 34, 35 | syl22anc 1183 |
. . . . 5
⊢ ((A ∈ Nn ∧ a ∈ (A +c 1c)) →
Tfin (A +c 1c) = (
Tfin A +c
1c)) |
37 | 36 | ex 423 |
. . . 4
⊢ (A ∈ Nn → (a ∈ (A
+c 1c) → Tfin (A
+c 1c) = ( Tfin A
+c 1c))) |
38 | 37 | exlimdv 1636 |
. . 3
⊢ (A ∈ Nn → (∃a a ∈ (A
+c 1c) → Tfin (A
+c 1c) = ( Tfin A
+c 1c))) |
39 | 1, 38 | syl5bi 208 |
. 2
⊢ (A ∈ Nn → ((A
+c 1c) ≠ ∅ → Tfin (A
+c 1c) = ( Tfin A
+c 1c))) |
40 | 39 | imp 418 |
1
⊢ ((A ∈ Nn ∧ (A +c 1c) ≠
∅) → Tfin (A
+c 1c) = ( Tfin A
+c 1c)) |