Proof of Theorem bnj150
Step | Hyp | Ref
| Expression |
1 | | 0ex 4718 |
. . . . . . . . . 10
⊢ ∅
∈ V |
2 | | bnj93 30187 |
. . . . . . . . . 10
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → pred(𝑥, 𝐴, 𝑅) ∈ V) |
3 | | funsng 5851 |
. . . . . . . . . 10
⊢ ((∅
∈ V ∧ pred(𝑥,
𝐴, 𝑅) ∈ V) → Fun {〈∅,
pred(𝑥, 𝐴, 𝑅)〉}) |
4 | 1, 2, 3 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → Fun {〈∅, pred(𝑥, 𝐴, 𝑅)〉}) |
5 | | bnj150.8 |
. . . . . . . . . 10
⊢ 𝐹 = {〈∅, pred(𝑥, 𝐴, 𝑅)〉} |
6 | 5 | funeqi 5824 |
. . . . . . . . 9
⊢ (Fun
𝐹 ↔ Fun
{〈∅, pred(𝑥,
𝐴, 𝑅)〉}) |
7 | 4, 6 | sylibr 223 |
. . . . . . . 8
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → Fun 𝐹) |
8 | 5 | bnj96 30189 |
. . . . . . . 8
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → dom 𝐹 = 1𝑜) |
9 | 7, 8 | bnj1422 30162 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐹 Fn 1𝑜) |
10 | 5 | bnj97 30190 |
. . . . . . . 8
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅)) |
11 | | bnj150.1 |
. . . . . . . . 9
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
12 | | bnj150.4 |
. . . . . . . . 9
⊢ (𝜑′ ↔
[1𝑜 / 𝑛]𝜑) |
13 | | bnj150.9 |
. . . . . . . . 9
⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′) |
14 | 11, 12, 13, 5 | bnj125 30196 |
. . . . . . . 8
⊢ (𝜑″ ↔ (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅)) |
15 | 10, 14 | sylibr 223 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝜑″) |
16 | 9, 15 | jca 553 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1𝑜 ∧ 𝜑″)) |
17 | | bnj98 30191 |
. . . . . . 7
⊢
∀𝑖 ∈
ω (suc 𝑖 ∈
1𝑜 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
18 | | bnj150.2 |
. . . . . . . 8
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
19 | | bnj150.5 |
. . . . . . . 8
⊢ (𝜓′ ↔
[1𝑜 / 𝑛]𝜓) |
20 | | bnj150.10 |
. . . . . . . 8
⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′) |
21 | 18, 19, 20, 5 | bnj126 30197 |
. . . . . . 7
⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1𝑜
→ (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
22 | 17, 21 | mpbir 220 |
. . . . . 6
⊢ 𝜓″ |
23 | 16, 22 | jctir 559 |
. . . . 5
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹 Fn 1𝑜 ∧ 𝜑″) ∧ 𝜓″)) |
24 | | df-3an 1033 |
. . . . 5
⊢ ((𝐹 Fn 1𝑜 ∧
𝜑″ ∧ 𝜓″) ↔ ((𝐹 Fn 1𝑜 ∧
𝜑″) ∧ 𝜓″)) |
25 | 23, 24 | sylibr 223 |
. . . 4
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1𝑜 ∧ 𝜑″ ∧ 𝜓″)) |
26 | | bnj150.11 |
. . . . 5
⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′) |
27 | | bnj150.3 |
. . . . . 6
⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
28 | | bnj150.7 |
. . . . . 6
⊢ (𝜁′ ↔
[1𝑜 / 𝑛]𝜁) |
29 | 27, 28, 12, 19 | bnj121 30194 |
. . . . 5
⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′))) |
30 | 5, 13, 20, 26, 29 | bnj124 30195 |
. . . 4
⊢ (𝜁″ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1𝑜 ∧ 𝜑″ ∧ 𝜓″))) |
31 | 25, 30 | mpbir 220 |
. . 3
⊢ 𝜁″ |
32 | 5 | bnj95 30188 |
. . . 4
⊢ 𝐹 ∈ V |
33 | | sbceq1a 3413 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝜁′ ↔ [𝐹 / 𝑓]𝜁′)) |
34 | 33, 26 | syl6bbr 277 |
. . . 4
⊢ (𝑓 = 𝐹 → (𝜁′ ↔ 𝜁″)) |
35 | 32, 34 | spcev 3273 |
. . 3
⊢ (𝜁″ → ∃𝑓𝜁′) |
36 | 31, 35 | ax-mp 5 |
. 2
⊢
∃𝑓𝜁′ |
37 | | bnj150.6 |
. . . 4
⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′))) |
38 | | 19.37v 1897 |
. . . 4
⊢
(∃𝑓((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′))) |
39 | 37, 38 | bitr4i 266 |
. . 3
⊢ (𝜃0 ↔ ∃𝑓((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1𝑜 ∧ 𝜑′ ∧ 𝜓′))) |
40 | 39, 29 | bnj133 30047 |
. 2
⊢ (𝜃0 ↔ ∃𝑓𝜁′) |
41 | 36, 40 | mpbir 220 |
1
⊢ 𝜃0 |