Step | Hyp | Ref
| Expression |
1 | | eqeq1 2177 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (𝑥 = ∅ ↔ 𝑢 = ∅)) |
2 | | eqeq1 2177 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → (𝑥 = suc 𝑦 ↔ 𝑢 = suc 𝑦)) |
3 | 2 | rexbidv 2471 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 ↔ ∃𝑦 ∈ 𝐴 𝑢 = suc 𝑦)) |
4 | 1, 3 | orbi12d 788 |
. . . . . 6
⊢ (𝑥 = 𝑢 → ((𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) ↔ (𝑢 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑢 = suc 𝑦))) |
5 | 4 | rspcv 2830 |
. . . . 5
⊢ (𝑢 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (𝑢 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑢 = suc 𝑦))) |
6 | | df-bj-ind 13924 |
. . . . . . . . 9
⊢ (Ind
𝑍 ↔ (∅ ∈
𝑍 ∧ ∀𝑣 ∈ 𝑍 suc 𝑣 ∈ 𝑍)) |
7 | 6 | simplbi 272 |
. . . . . . . 8
⊢ (Ind
𝑍 → ∅ ∈
𝑍) |
8 | | eleq1 2233 |
. . . . . . . 8
⊢ (𝑢 = ∅ → (𝑢 ∈ 𝑍 ↔ ∅ ∈ 𝑍)) |
9 | 7, 8 | syl5ibr 155 |
. . . . . . 7
⊢ (𝑢 = ∅ → (Ind 𝑍 → 𝑢 ∈ 𝑍)) |
10 | 9 | a1dd 48 |
. . . . . 6
⊢ (𝑢 = ∅ → (Ind 𝑍 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → 𝑢 ∈ 𝑍))) |
11 | | vex 2733 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
12 | 11 | sucid 4400 |
. . . . . . . . 9
⊢ 𝑦 ∈ suc 𝑦 |
13 | | eleq2 2234 |
. . . . . . . . . 10
⊢ (suc
𝑦 = 𝑢 → (𝑦 ∈ suc 𝑦 ↔ 𝑦 ∈ 𝑢)) |
14 | 13 | eqcoms 2173 |
. . . . . . . . 9
⊢ (𝑢 = suc 𝑦 → (𝑦 ∈ suc 𝑦 ↔ 𝑦 ∈ 𝑢)) |
15 | 12, 14 | mpbii 147 |
. . . . . . . 8
⊢ (𝑢 = suc 𝑦 → 𝑦 ∈ 𝑢) |
16 | | eleq1 2233 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑦 → (𝑡 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
17 | | eleq1 2233 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑦 → (𝑡 ∈ 𝑍 ↔ 𝑦 ∈ 𝑍)) |
18 | 16, 17 | imbi12d 233 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑦 → ((𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) ↔ (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝑍))) |
19 | 18 | rspcv 2830 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑢 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝑍))) |
20 | | bj-indsuc 13925 |
. . . . . . . . . . . 12
⊢ (Ind
𝑍 → (𝑦 ∈ 𝑍 → suc 𝑦 ∈ 𝑍)) |
21 | | eleq1a 2242 |
. . . . . . . . . . . 12
⊢ (suc
𝑦 ∈ 𝑍 → (𝑢 = suc 𝑦 → 𝑢 ∈ 𝑍)) |
22 | 20, 21 | syl6com 35 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑍 → (Ind 𝑍 → (𝑢 = suc 𝑦 → 𝑢 ∈ 𝑍))) |
23 | 19, 22 | syl8 71 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑢 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → (𝑦 ∈ 𝐴 → (Ind 𝑍 → (𝑢 = suc 𝑦 → 𝑢 ∈ 𝑍))))) |
24 | 23 | com13 80 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → (𝑦 ∈ 𝑢 → (Ind 𝑍 → (𝑢 = suc 𝑦 → 𝑢 ∈ 𝑍))))) |
25 | 24 | com25 91 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (𝑢 = suc 𝑦 → (𝑦 ∈ 𝑢 → (Ind 𝑍 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → 𝑢 ∈ 𝑍))))) |
26 | 15, 25 | mpdi 43 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → (𝑢 = suc 𝑦 → (Ind 𝑍 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → 𝑢 ∈ 𝑍)))) |
27 | 26 | rexlimiv 2581 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐴 𝑢 = suc 𝑦 → (Ind 𝑍 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → 𝑢 ∈ 𝑍))) |
28 | 10, 27 | jaoi 711 |
. . . . 5
⊢ ((𝑢 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑢 = suc 𝑦) → (Ind 𝑍 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → 𝑢 ∈ 𝑍))) |
29 | 5, 28 | syl6 33 |
. . . 4
⊢ (𝑢 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → 𝑢 ∈ 𝑍)))) |
30 | 29 | com3l 81 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → (𝑢 ∈ 𝐴 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → 𝑢 ∈ 𝑍)))) |
31 | 30 | alrimdv 1869 |
. 2
⊢
(∀𝑥 ∈
𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → ∀𝑢(𝑢 ∈ 𝐴 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → 𝑢 ∈ 𝑍)))) |
32 | | bi2.04 247 |
. . 3
⊢ ((𝑢 ∈ 𝐴 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → 𝑢 ∈ 𝑍)) ↔ (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → (𝑢 ∈ 𝐴 → 𝑢 ∈ 𝑍))) |
33 | 32 | albii 1463 |
. 2
⊢
(∀𝑢(𝑢 ∈ 𝐴 → (∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → 𝑢 ∈ 𝑍)) ↔ ∀𝑢(∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → (𝑢 ∈ 𝐴 → 𝑢 ∈ 𝑍))) |
34 | 31, 33 | syl6ib 160 |
1
⊢
(∀𝑥 ∈
𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → ∀𝑢(∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → (𝑢 ∈ 𝐴 → 𝑢 ∈ 𝑍)))) |