Step | Hyp | Ref
| Expression |
1 | | eqeq1 2043 |
. . . . . . 7
⊢ (x = u →
(x = ∅ ↔ u = ∅)) |
2 | | eqeq1 2043 |
. . . . . . . 8
⊢ (x = u →
(x = suc y ↔ u = suc
y)) |
3 | 2 | rexbidv 2321 |
. . . . . . 7
⊢ (x = u →
(∃y
∈ A
x = suc y ↔ ∃y ∈ A u = suc y)) |
4 | 1, 3 | orbi12d 706 |
. . . . . 6
⊢ (x = u →
((x = ∅
∨ ∃y ∈ A x = suc
y) ↔ (u = ∅ ∨ ∃y ∈ A u = suc y))) |
5 | 4 | rspcv 2646 |
. . . . 5
⊢ (u ∈ A → (∀x ∈ A (x = ∅ ∨ ∃y ∈ A x = suc y)
→ (u = ∅
∨ ∃y ∈ A u = suc
y))) |
6 | | df-bj-ind 9386 |
. . . . . . . . 9
⊢ (Ind
𝑍 ↔ (∅ ∈ 𝑍 ∧ ∀v ∈ 𝑍 suc v
∈ 𝑍)) |
7 | 6 | simplbi 259 |
. . . . . . . 8
⊢ (Ind
𝑍 → ∅ ∈ 𝑍) |
8 | | eleq1 2097 |
. . . . . . . 8
⊢ (u = ∅ → (u ∈ 𝑍 ↔ ∅ ∈ 𝑍)) |
9 | 7, 8 | syl5ibr 145 |
. . . . . . 7
⊢ (u = ∅ → (Ind 𝑍 → u ∈ 𝑍)) |
10 | 9 | a1dd 42 |
. . . . . 6
⊢ (u = ∅ → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍))) |
11 | | vex 2554 |
. . . . . . . . . 10
⊢ y ∈
V |
12 | 11 | sucid 4120 |
. . . . . . . . 9
⊢ y ∈ suc y |
13 | | eleq2 2098 |
. . . . . . . . . 10
⊢ (suc
y = u
→ (y ∈ suc y ↔
y ∈
u)) |
14 | 13 | eqcoms 2040 |
. . . . . . . . 9
⊢ (u = suc y →
(y ∈ suc
y ↔ y ∈ u)) |
15 | 12, 14 | mpbii 136 |
. . . . . . . 8
⊢ (u = suc y →
y ∈
u) |
16 | | eleq1 2097 |
. . . . . . . . . . . . 13
⊢ (𝑡 = y → (𝑡 ∈ A ↔ y ∈ A)) |
17 | | eleq1 2097 |
. . . . . . . . . . . . 13
⊢ (𝑡 = y → (𝑡 ∈ 𝑍 ↔ y ∈ 𝑍)) |
18 | 16, 17 | imbi12d 223 |
. . . . . . . . . . . 12
⊢ (𝑡 = y → ((𝑡 ∈ A → 𝑡 ∈ 𝑍) ↔ (y ∈ A → y ∈ 𝑍))) |
19 | 18 | rspcv 2646 |
. . . . . . . . . . 11
⊢ (y ∈ u → (∀𝑡 ∈ u (𝑡 ∈ A →
𝑡 ∈ 𝑍) → (y ∈ A → y ∈ 𝑍))) |
20 | | bj-indsuc 9387 |
. . . . . . . . . . . 12
⊢ (Ind
𝑍 → (y ∈ 𝑍 → suc y ∈ 𝑍)) |
21 | | eleq1a 2106 |
. . . . . . . . . . . 12
⊢ (suc
y ∈ 𝑍 → (u = suc y →
u ∈ 𝑍)) |
22 | 20, 21 | syl6com 31 |
. . . . . . . . . . 11
⊢ (y ∈ 𝑍 → (Ind 𝑍 → (u = suc y →
u ∈ 𝑍))) |
23 | 19, 22 | syl8 65 |
. . . . . . . . . 10
⊢ (y ∈ u → (∀𝑡 ∈ u (𝑡 ∈ A →
𝑡 ∈ 𝑍) → (y ∈ A → (Ind 𝑍 → (u = suc y →
u ∈ 𝑍))))) |
24 | 23 | com13 74 |
. . . . . . . . 9
⊢ (y ∈ A → (∀𝑡 ∈ u (𝑡 ∈ A →
𝑡 ∈ 𝑍) → (y ∈ u → (Ind 𝑍 → (u = suc y →
u ∈ 𝑍))))) |
25 | 24 | com25 85 |
. . . . . . . 8
⊢ (y ∈ A → (u =
suc y → (y ∈ u → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍))))) |
26 | 15, 25 | mpdi 38 |
. . . . . . 7
⊢ (y ∈ A → (u =
suc y → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)))) |
27 | 26 | rexlimiv 2421 |
. . . . . 6
⊢ (∃y ∈ A u = suc y →
(Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍))) |
28 | 10, 27 | jaoi 635 |
. . . . 5
⊢
((u = ∅
∨ ∃y ∈ A u = suc
y) → (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍))) |
29 | 5, 28 | syl6 29 |
. . . 4
⊢ (u ∈ A → (∀x ∈ A (x = ∅ ∨ ∃y ∈ A x = suc y)
→ (Ind 𝑍 → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)))) |
30 | 29 | com3l 75 |
. . 3
⊢ (∀x ∈ A (x = ∅ ∨ ∃y ∈ A x = suc y)
→ (Ind 𝑍 →
(u ∈
A → (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)))) |
31 | 30 | alrimdv 1753 |
. 2
⊢ (∀x ∈ A (x = ∅ ∨ ∃y ∈ A x = suc y)
→ (Ind 𝑍 → ∀u(u ∈ A → (∀𝑡 ∈ u (𝑡 ∈ A →
𝑡 ∈ 𝑍) → u ∈ 𝑍)))) |
32 | | bi2.04 237 |
. . 3
⊢
((u ∈ A →
(∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → u ∈ 𝑍)) ↔ (∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → (u ∈ A → u ∈ 𝑍))) |
33 | 32 | albii 1356 |
. 2
⊢ (∀u(u ∈ A → (∀𝑡 ∈ u (𝑡 ∈ A →
𝑡 ∈ 𝑍) → u ∈ 𝑍)) ↔ ∀u(∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → (u ∈ A → u ∈ 𝑍))) |
34 | 31, 33 | syl6ib 150 |
1
⊢ (∀x ∈ A (x = ∅ ∨ ∃y ∈ A x = suc y)
→ (Ind 𝑍 → ∀u(∀𝑡 ∈ u (𝑡 ∈ A → 𝑡 ∈ 𝑍) → (u ∈ A → u ∈ 𝑍)))) |