| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . 3
⊢ (𝑣 = ∅ → (𝐹‘𝑣) = (𝐹‘∅)) |
| 2 | | suceq 6450 |
. . . 4
⊢ (𝑣 = ∅ → suc 𝑣 = suc ∅) |
| 3 | 2 | fveq2d 6910 |
. . 3
⊢ (𝑣 = ∅ → (𝐹‘suc 𝑣) = (𝐹‘suc ∅)) |
| 4 | 1, 3 | sseq12d 4017 |
. 2
⊢ (𝑣 = ∅ → ((𝐹‘𝑣) ⊆ (𝐹‘suc 𝑣) ↔ (𝐹‘∅) ⊆ (𝐹‘suc ∅))) |
| 5 | | fveq2 6906 |
. . 3
⊢ (𝑣 = 𝑢 → (𝐹‘𝑣) = (𝐹‘𝑢)) |
| 6 | | suceq 6450 |
. . . 4
⊢ (𝑣 = 𝑢 → suc 𝑣 = suc 𝑢) |
| 7 | 6 | fveq2d 6910 |
. . 3
⊢ (𝑣 = 𝑢 → (𝐹‘suc 𝑣) = (𝐹‘suc 𝑢)) |
| 8 | 5, 7 | sseq12d 4017 |
. 2
⊢ (𝑣 = 𝑢 → ((𝐹‘𝑣) ⊆ (𝐹‘suc 𝑣) ↔ (𝐹‘𝑢) ⊆ (𝐹‘suc 𝑢))) |
| 9 | | fveq2 6906 |
. . 3
⊢ (𝑣 = suc 𝑢 → (𝐹‘𝑣) = (𝐹‘suc 𝑢)) |
| 10 | | suceq 6450 |
. . . 4
⊢ (𝑣 = suc 𝑢 → suc 𝑣 = suc suc 𝑢) |
| 11 | 10 | fveq2d 6910 |
. . 3
⊢ (𝑣 = suc 𝑢 → (𝐹‘suc 𝑣) = (𝐹‘suc suc 𝑢)) |
| 12 | 9, 11 | sseq12d 4017 |
. 2
⊢ (𝑣 = suc 𝑢 → ((𝐹‘𝑣) ⊆ (𝐹‘suc 𝑣) ↔ (𝐹‘suc 𝑢) ⊆ (𝐹‘suc suc 𝑢))) |
| 13 | | fveq2 6906 |
. . 3
⊢ (𝑣 = 𝐴 → (𝐹‘𝑣) = (𝐹‘𝐴)) |
| 14 | | suceq 6450 |
. . . 4
⊢ (𝑣 = 𝐴 → suc 𝑣 = suc 𝐴) |
| 15 | 14 | fveq2d 6910 |
. . 3
⊢ (𝑣 = 𝐴 → (𝐹‘suc 𝑣) = (𝐹‘suc 𝐴)) |
| 16 | 13, 15 | sseq12d 4017 |
. 2
⊢ (𝑣 = 𝐴 → ((𝐹‘𝑣) ⊆ (𝐹‘suc 𝑣) ↔ (𝐹‘𝐴) ⊆ (𝐹‘suc 𝐴))) |
| 17 | | inf3lem.1 |
. . . 4
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) |
| 18 | | inf3lem.2 |
. . . 4
⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) |
| 19 | | inf3lem.3 |
. . . 4
⊢ 𝐴 ∈ V |
| 20 | 17, 18, 19, 19 | inf3lemb 9665 |
. . 3
⊢ (𝐹‘∅) =
∅ |
| 21 | | 0ss 4400 |
. . 3
⊢ ∅
⊆ (𝐹‘suc
∅) |
| 22 | 20, 21 | eqsstri 4030 |
. 2
⊢ (𝐹‘∅) ⊆ (𝐹‘suc
∅) |
| 23 | | sstr2 3990 |
. . . . . . . 8
⊢ ((𝑣 ∩ 𝑥) ⊆ (𝐹‘𝑢) → ((𝐹‘𝑢) ⊆ (𝐹‘suc 𝑢) → (𝑣 ∩ 𝑥) ⊆ (𝐹‘suc 𝑢))) |
| 24 | 23 | com12 32 |
. . . . . . 7
⊢ ((𝐹‘𝑢) ⊆ (𝐹‘suc 𝑢) → ((𝑣 ∩ 𝑥) ⊆ (𝐹‘𝑢) → (𝑣 ∩ 𝑥) ⊆ (𝐹‘suc 𝑢))) |
| 25 | 24 | anim2d 612 |
. . . . . 6
⊢ ((𝐹‘𝑢) ⊆ (𝐹‘suc 𝑢) → ((𝑣 ∈ 𝑥 ∧ (𝑣 ∩ 𝑥) ⊆ (𝐹‘𝑢)) → (𝑣 ∈ 𝑥 ∧ (𝑣 ∩ 𝑥) ⊆ (𝐹‘suc 𝑢)))) |
| 26 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
| 27 | 17, 18, 26, 19 | inf3lemc 9666 |
. . . . . . . . 9
⊢ (𝑢 ∈ ω → (𝐹‘suc 𝑢) = (𝐺‘(𝐹‘𝑢))) |
| 28 | 27 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑢 ∈ ω → (𝑣 ∈ (𝐹‘suc 𝑢) ↔ 𝑣 ∈ (𝐺‘(𝐹‘𝑢)))) |
| 29 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑣 ∈ V |
| 30 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐹‘𝑢) ∈ V |
| 31 | 17, 18, 29, 30 | inf3lema 9664 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝐺‘(𝐹‘𝑢)) ↔ (𝑣 ∈ 𝑥 ∧ (𝑣 ∩ 𝑥) ⊆ (𝐹‘𝑢))) |
| 32 | 28, 31 | bitrdi 287 |
. . . . . . 7
⊢ (𝑢 ∈ ω → (𝑣 ∈ (𝐹‘suc 𝑢) ↔ (𝑣 ∈ 𝑥 ∧ (𝑣 ∩ 𝑥) ⊆ (𝐹‘𝑢)))) |
| 33 | | peano2b 7904 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ω ↔ suc 𝑢 ∈
ω) |
| 34 | 26 | sucex 7826 |
. . . . . . . . . . 11
⊢ suc 𝑢 ∈ V |
| 35 | 17, 18, 34, 19 | inf3lemc 9666 |
. . . . . . . . . 10
⊢ (suc
𝑢 ∈ ω →
(𝐹‘suc suc 𝑢) = (𝐺‘(𝐹‘suc 𝑢))) |
| 36 | 33, 35 | sylbi 217 |
. . . . . . . . 9
⊢ (𝑢 ∈ ω → (𝐹‘suc suc 𝑢) = (𝐺‘(𝐹‘suc 𝑢))) |
| 37 | 36 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑢 ∈ ω → (𝑣 ∈ (𝐹‘suc suc 𝑢) ↔ 𝑣 ∈ (𝐺‘(𝐹‘suc 𝑢)))) |
| 38 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐹‘suc 𝑢) ∈ V |
| 39 | 17, 18, 29, 38 | inf3lema 9664 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝐺‘(𝐹‘suc 𝑢)) ↔ (𝑣 ∈ 𝑥 ∧ (𝑣 ∩ 𝑥) ⊆ (𝐹‘suc 𝑢))) |
| 40 | 37, 39 | bitrdi 287 |
. . . . . . 7
⊢ (𝑢 ∈ ω → (𝑣 ∈ (𝐹‘suc suc 𝑢) ↔ (𝑣 ∈ 𝑥 ∧ (𝑣 ∩ 𝑥) ⊆ (𝐹‘suc 𝑢)))) |
| 41 | 32, 40 | imbi12d 344 |
. . . . . 6
⊢ (𝑢 ∈ ω → ((𝑣 ∈ (𝐹‘suc 𝑢) → 𝑣 ∈ (𝐹‘suc suc 𝑢)) ↔ ((𝑣 ∈ 𝑥 ∧ (𝑣 ∩ 𝑥) ⊆ (𝐹‘𝑢)) → (𝑣 ∈ 𝑥 ∧ (𝑣 ∩ 𝑥) ⊆ (𝐹‘suc 𝑢))))) |
| 42 | 25, 41 | imbitrrid 246 |
. . . . 5
⊢ (𝑢 ∈ ω → ((𝐹‘𝑢) ⊆ (𝐹‘suc 𝑢) → (𝑣 ∈ (𝐹‘suc 𝑢) → 𝑣 ∈ (𝐹‘suc suc 𝑢)))) |
| 43 | 42 | imp 406 |
. . . 4
⊢ ((𝑢 ∈ ω ∧ (𝐹‘𝑢) ⊆ (𝐹‘suc 𝑢)) → (𝑣 ∈ (𝐹‘suc 𝑢) → 𝑣 ∈ (𝐹‘suc suc 𝑢))) |
| 44 | 43 | ssrdv 3989 |
. . 3
⊢ ((𝑢 ∈ ω ∧ (𝐹‘𝑢) ⊆ (𝐹‘suc 𝑢)) → (𝐹‘suc 𝑢) ⊆ (𝐹‘suc suc 𝑢)) |
| 45 | 44 | ex 412 |
. 2
⊢ (𝑢 ∈ ω → ((𝐹‘𝑢) ⊆ (𝐹‘suc 𝑢) → (𝐹‘suc 𝑢) ⊆ (𝐹‘suc suc 𝑢))) |
| 46 | 4, 8, 12, 16, 22, 45 | finds 7918 |
1
⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ (𝐹‘suc 𝐴)) |