Proof of Theorem bnj996
| Step | Hyp | Ref
| Expression |
| 1 | | bnj996.4 |
. . . . 5
⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) |
| 2 | | bnj996.1 |
. . . . . 6
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
| 3 | | bnj996.2 |
. . . . . 6
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 4 | | bnj996.13 |
. . . . . 6
⊢ 𝐷 = (ω ∖
{∅}) |
| 5 | | bnj996.14 |
. . . . . 6
⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} |
| 6 | | bnj996.3 |
. . . . . 6
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
| 7 | 2, 3, 4, 5, 6 | bnj917 34948 |
. . . . 5
⊢ (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) |
| 8 | 1, 7 | bnj771 34778 |
. . . 4
⊢ (𝜃 → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) |
| 9 | | 3anass 1095 |
. . . . . 6
⊢ ((𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)) ↔ (𝜒 ∧ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)))) |
| 10 | | bnj996.6 |
. . . . . . 7
⊢ (𝜂 ↔ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) |
| 11 | 10 | anbi2i 623 |
. . . . . 6
⊢ ((𝜒 ∧ 𝜂) ↔ (𝜒 ∧ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)))) |
| 12 | 9, 11 | bitr4i 278 |
. . . . 5
⊢ ((𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)) ↔ (𝜒 ∧ 𝜂)) |
| 13 | 12 | 3exbii 1850 |
. . . 4
⊢
(∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)) ↔ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝜂)) |
| 14 | 8, 13 | sylib 218 |
. . 3
⊢ (𝜃 → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝜂)) |
| 15 | | bnj996.5 |
. . . . . . . . . 10
⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) |
| 16 | 6, 4, 15 | bnj986 34969 |
. . . . . . . . 9
⊢ (𝜒 → ∃𝑚∃𝑝𝜏) |
| 17 | 16 | ancli 548 |
. . . . . . . 8
⊢ (𝜒 → (𝜒 ∧ ∃𝑚∃𝑝𝜏)) |
| 18 | | 19.42vv 1957 |
. . . . . . . 8
⊢
(∃𝑚∃𝑝(𝜒 ∧ 𝜏) ↔ (𝜒 ∧ ∃𝑚∃𝑝𝜏)) |
| 19 | 17, 18 | sylibr 234 |
. . . . . . 7
⊢ (𝜒 → ∃𝑚∃𝑝(𝜒 ∧ 𝜏)) |
| 20 | 19 | anim1i 615 |
. . . . . 6
⊢ ((𝜒 ∧ 𝜂) → (∃𝑚∃𝑝(𝜒 ∧ 𝜏) ∧ 𝜂)) |
| 21 | | 19.41vv 1950 |
. . . . . 6
⊢
(∃𝑚∃𝑝((𝜒 ∧ 𝜏) ∧ 𝜂) ↔ (∃𝑚∃𝑝(𝜒 ∧ 𝜏) ∧ 𝜂)) |
| 22 | 20, 21 | sylibr 234 |
. . . . 5
⊢ ((𝜒 ∧ 𝜂) → ∃𝑚∃𝑝((𝜒 ∧ 𝜏) ∧ 𝜂)) |
| 23 | | df-3an 1089 |
. . . . . 6
⊢ ((𝜒 ∧ 𝜏 ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜂)) |
| 24 | 23 | 2exbii 1849 |
. . . . 5
⊢
(∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂) ↔ ∃𝑚∃𝑝((𝜒 ∧ 𝜏) ∧ 𝜂)) |
| 25 | 22, 24 | sylibr 234 |
. . . 4
⊢ ((𝜒 ∧ 𝜂) → ∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂)) |
| 26 | 25 | 2eximi 1836 |
. . 3
⊢
(∃𝑛∃𝑖(𝜒 ∧ 𝜂) → ∃𝑛∃𝑖∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂)) |
| 27 | 14, 26 | bnj593 34759 |
. 2
⊢ (𝜃 → ∃𝑓∃𝑛∃𝑖∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂)) |
| 28 | | 19.37v 1991 |
. . . . . . . . . 10
⊢
(∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) ↔ (𝜃 → ∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂))) |
| 29 | 28 | exbii 1848 |
. . . . . . . . 9
⊢
(∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) ↔ ∃𝑚(𝜃 → ∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂))) |
| 30 | 29 | bnj132 34740 |
. . . . . . . 8
⊢
(∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) ↔ (𝜃 → ∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂))) |
| 31 | 30 | exbii 1848 |
. . . . . . 7
⊢
(∃𝑖∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) ↔ ∃𝑖(𝜃 → ∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂))) |
| 32 | 31 | bnj132 34740 |
. . . . . 6
⊢
(∃𝑖∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) ↔ (𝜃 → ∃𝑖∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂))) |
| 33 | 32 | exbii 1848 |
. . . . 5
⊢
(∃𝑛∃𝑖∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) ↔ ∃𝑛(𝜃 → ∃𝑖∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂))) |
| 34 | 33 | bnj132 34740 |
. . . 4
⊢
(∃𝑛∃𝑖∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) ↔ (𝜃 → ∃𝑛∃𝑖∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂))) |
| 35 | 34 | exbii 1848 |
. . 3
⊢
(∃𝑓∃𝑛∃𝑖∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) ↔ ∃𝑓(𝜃 → ∃𝑛∃𝑖∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂))) |
| 36 | 35 | bnj132 34740 |
. 2
⊢
(∃𝑓∃𝑛∃𝑖∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) ↔ (𝜃 → ∃𝑓∃𝑛∃𝑖∃𝑚∃𝑝(𝜒 ∧ 𝜏 ∧ 𝜂))) |
| 37 | 27, 36 | mpbir 231 |
1
⊢
∃𝑓∃𝑛∃𝑖∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂)) |