Proof of Theorem bnj1033
Step | Hyp | Ref
| Expression |
1 | | bnj1033.1 |
. . . . 5
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
2 | | bnj1033.2 |
. . . . 5
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
3 | | bnj1033.8 |
. . . . 5
⊢ 𝐷 = (ω ∖
{∅}) |
4 | | bnj1033.9 |
. . . . 5
⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} |
5 | | bnj1033.3 |
. . . . 5
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
6 | 1, 2, 3, 4, 5 | bnj983 32910 |
. . . 4
⊢ (𝑧 ∈ trCl(𝑋, 𝐴, 𝑅) ↔ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) |
7 | | 19.42v 1960 |
. . . . . . . . . 10
⊢
(∃𝑖((𝜃 ∧ 𝜏) ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ((𝜃 ∧ 𝜏) ∧ ∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
8 | | df-3an 1087 |
. . . . . . . . . . 11
⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ((𝜃 ∧ 𝜏) ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
9 | 8 | exbii 1853 |
. . . . . . . . . 10
⊢
(∃𝑖(𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ∃𝑖((𝜃 ∧ 𝜏) ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
10 | | df-3an 1087 |
. . . . . . . . . 10
⊢ ((𝜃 ∧ 𝜏 ∧ ∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ((𝜃 ∧ 𝜏) ∧ ∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
11 | 7, 9, 10 | 3bitr4i 302 |
. . . . . . . . 9
⊢
(∃𝑖(𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ (𝜃 ∧ 𝜏 ∧ ∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
12 | 11 | exbii 1853 |
. . . . . . . 8
⊢
(∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ∃𝑛(𝜃 ∧ 𝜏 ∧ ∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
13 | | 19.42v 1960 |
. . . . . . . . 9
⊢
(∃𝑛((𝜃 ∧ 𝜏) ∧ ∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ((𝜃 ∧ 𝜏) ∧ ∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
14 | 10 | exbii 1853 |
. . . . . . . . 9
⊢
(∃𝑛(𝜃 ∧ 𝜏 ∧ ∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ∃𝑛((𝜃 ∧ 𝜏) ∧ ∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
15 | | df-3an 1087 |
. . . . . . . . 9
⊢ ((𝜃 ∧ 𝜏 ∧ ∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ((𝜃 ∧ 𝜏) ∧ ∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
16 | 13, 14, 15 | 3bitr4i 302 |
. . . . . . . 8
⊢
(∃𝑛(𝜃 ∧ 𝜏 ∧ ∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ (𝜃 ∧ 𝜏 ∧ ∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
17 | 12, 16 | bitri 274 |
. . . . . . 7
⊢
(∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ (𝜃 ∧ 𝜏 ∧ ∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
18 | 17 | exbii 1853 |
. . . . . 6
⊢
(∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ∃𝑓(𝜃 ∧ 𝜏 ∧ ∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
19 | | 19.42v 1960 |
. . . . . . 7
⊢
(∃𝑓((𝜃 ∧ 𝜏) ∧ ∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ((𝜃 ∧ 𝜏) ∧ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
20 | 15 | exbii 1853 |
. . . . . . 7
⊢
(∃𝑓(𝜃 ∧ 𝜏 ∧ ∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ∃𝑓((𝜃 ∧ 𝜏) ∧ ∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
21 | | df-3an 1087 |
. . . . . . 7
⊢ ((𝜃 ∧ 𝜏 ∧ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ ((𝜃 ∧ 𝜏) ∧ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
22 | 19, 20, 21 | 3bitr4i 302 |
. . . . . 6
⊢
(∃𝑓(𝜃 ∧ 𝜏 ∧ ∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ (𝜃 ∧ 𝜏 ∧ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
23 | 18, 22 | bitri 274 |
. . . . 5
⊢
(∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) ↔ (𝜃 ∧ 𝜏 ∧ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
24 | | bnj255 32663 |
. . . . . . . 8
⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) ↔ (𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝜁))) |
25 | | bnj1033.7 |
. . . . . . . . . . 11
⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) |
26 | 25 | anbi2i 622 |
. . . . . . . . . 10
⊢ ((𝜒 ∧ 𝜁) ↔ (𝜒 ∧ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
27 | | 3anass 1093 |
. . . . . . . . . 10
⊢ ((𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)) ↔ (𝜒 ∧ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
28 | 26, 27 | bitr4i 277 |
. . . . . . . . 9
⊢ ((𝜒 ∧ 𝜁) ↔ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) |
29 | 28 | 3anbi3i 1157 |
. . . . . . . 8
⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝜁)) ↔ (𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
30 | 24, 29 | bitri 274 |
. . . . . . 7
⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) ↔ (𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
31 | 30 | 3exbii 1855 |
. . . . . 6
⊢
(∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) ↔ ∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))) |
32 | | bnj1033.10 |
. . . . . 6
⊢
(∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵) |
33 | 31, 32 | sylbir 234 |
. . . . 5
⊢
(∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) → 𝑧 ∈ 𝐵) |
34 | 23, 33 | sylbir 234 |
. . . 4
⊢ ((𝜃 ∧ 𝜏 ∧ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖))) → 𝑧 ∈ 𝐵) |
35 | 6, 34 | syl3an3b 1403 |
. . 3
⊢ ((𝜃 ∧ 𝜏 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) → 𝑧 ∈ 𝐵) |
36 | 35 | 3expia 1119 |
. 2
⊢ ((𝜃 ∧ 𝜏) → (𝑧 ∈ trCl(𝑋, 𝐴, 𝑅) → 𝑧 ∈ 𝐵)) |
37 | 36 | ssrdv 3931 |
1
⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) |