Proof of Theorem bnj150
| Step | Hyp | Ref
| Expression |
| 1 | | bnj150.8 |
. . . 4
⊢ 𝐹 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉} |
| 2 | 1 | bnj95 34878 |
. . 3
⊢ 𝐹 ∈ V |
| 3 | | sbceq1a 3799 |
. . . 4
⊢ (𝑓 = 𝐹 → (𝜁′ ↔ [𝐹 / 𝑓]𝜁′)) |
| 4 | | bnj150.11 |
. . . 4
⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′) |
| 5 | 3, 4 | bitr4di 289 |
. . 3
⊢ (𝑓 = 𝐹 → (𝜁′ ↔ 𝜁″)) |
| 6 | | 0ex 5307 |
. . . . . . . . 9
⊢ ∅
∈ V |
| 7 | | bnj93 34877 |
. . . . . . . . 9
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → pred(𝑥, 𝐴, 𝑅) ∈ V) |
| 8 | | funsng 6617 |
. . . . . . . . 9
⊢ ((∅
∈ V ∧ pred(𝑥,
𝐴, 𝑅) ∈ V) → Fun {〈∅,
pred(𝑥, 𝐴, 𝑅)〉}) |
| 9 | 6, 7, 8 | sylancr 587 |
. . . . . . . 8
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → Fun {〈∅, pred(𝑥, 𝐴, 𝑅)〉}) |
| 10 | 1 | funeqi 6587 |
. . . . . . . 8
⊢ (Fun
𝐹 ↔ Fun
{〈∅, pred(𝑥,
𝐴, 𝑅)〉}) |
| 11 | 9, 10 | sylibr 234 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → Fun 𝐹) |
| 12 | 1 | bnj96 34879 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → dom 𝐹 = 1o) |
| 13 | 11, 12 | bnj1422 34851 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐹 Fn 1o) |
| 14 | 1 | bnj97 34880 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅)) |
| 15 | | bnj150.1 |
. . . . . . . 8
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
| 16 | | bnj150.4 |
. . . . . . . 8
⊢ (𝜑′ ↔
[1o / 𝑛]𝜑) |
| 17 | | bnj150.9 |
. . . . . . . 8
⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′) |
| 18 | 15, 16, 17, 1 | bnj125 34886 |
. . . . . . 7
⊢ (𝜑″ ↔ (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅)) |
| 19 | 14, 18 | sylibr 234 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝜑″) |
| 20 | 13, 19 | jca 511 |
. . . . 5
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1o ∧ 𝜑″)) |
| 21 | | bnj98 34881 |
. . . . . 6
⊢
∀𝑖 ∈
ω (suc 𝑖 ∈
1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
| 22 | | bnj150.2 |
. . . . . . 7
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 23 | | bnj150.5 |
. . . . . . 7
⊢ (𝜓′ ↔
[1o / 𝑛]𝜓) |
| 24 | | bnj150.10 |
. . . . . . 7
⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′) |
| 25 | 22, 23, 24, 1 | bnj126 34887 |
. . . . . 6
⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o →
(𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 26 | 21, 25 | mpbir 231 |
. . . . 5
⊢ 𝜓″ |
| 27 | | df-3an 1089 |
. . . . 5
⊢ ((𝐹 Fn 1o ∧ 𝜑″ ∧ 𝜓″) ↔ ((𝐹 Fn 1o ∧ 𝜑″) ∧ 𝜓″)) |
| 28 | 20, 26, 27 | sylanblrc 590 |
. . . 4
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1o ∧ 𝜑″ ∧ 𝜓″)) |
| 29 | | bnj150.3 |
. . . . . 6
⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
| 30 | | bnj150.7 |
. . . . . 6
⊢ (𝜁′ ↔
[1o / 𝑛]𝜁) |
| 31 | 29, 30, 16, 23 | bnj121 34884 |
. . . . 5
⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) |
| 32 | 1, 17, 24, 4, 31 | bnj124 34885 |
. . . 4
⊢ (𝜁″ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1o ∧ 𝜑″ ∧ 𝜓″))) |
| 33 | 28, 32 | mpbir 231 |
. . 3
⊢ 𝜁″ |
| 34 | 2, 5, 33 | ceqsexv2d 3533 |
. 2
⊢
∃𝑓𝜁′ |
| 35 | | bnj150.6 |
. . . 4
⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) |
| 36 | | 19.37v 1991 |
. . . 4
⊢
(∃𝑓((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) |
| 37 | 35, 36 | bitr4i 278 |
. . 3
⊢ (𝜃0 ↔ ∃𝑓((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))) |
| 38 | 37, 31 | bnj133 34741 |
. 2
⊢ (𝜃0 ↔ ∃𝑓𝜁′) |
| 39 | 34, 38 | mpbir 231 |
1
⊢ 𝜃0 |