Proof of Theorem bnj981
Step | Hyp | Ref
| Expression |
1 | | nfv 1917 |
. . . 4
⊢
Ⅎ𝑦 𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) |
2 | | bnj981.2 |
. . . . . . . . . . . 12
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
3 | | nfcv 2907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦ω |
4 | | nfv 1917 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 suc 𝑖 ∈ 𝑛 |
5 | | nfiu1 4959 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) |
6 | 5 | nfeq2 2924 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) |
7 | 4, 6 | nfim 1899 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
8 | 3, 7 | nfralw 3150 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
9 | 2, 8 | nfxfr 1855 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝜓 |
10 | 9 | nf5ri 2188 |
. . . . . . . . . 10
⊢ (𝜓 → ∀𝑦𝜓) |
11 | | bnj981.5 |
. . . . . . . . . 10
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
12 | 10, 11 | bnj1096 32748 |
. . . . . . . . 9
⊢ (𝜒 → ∀𝑦𝜒) |
13 | 12 | nf5i 2142 |
. . . . . . . 8
⊢
Ⅎ𝑦𝜒 |
14 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑖 ∈ 𝑛 |
15 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑍 ∈ (𝑓‘𝑖) |
16 | 13, 14, 15 | nf3an 1904 |
. . . . . . 7
⊢
Ⅎ𝑦(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)) |
17 | 16 | nfex 2318 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)) |
18 | 17 | nfex 2318 |
. . . . 5
⊢
Ⅎ𝑦∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)) |
19 | 18 | nfex 2318 |
. . . 4
⊢
Ⅎ𝑦∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)) |
20 | 1, 19 | nfim 1899 |
. . 3
⊢
Ⅎ𝑦(𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖))) |
21 | | eleq1 2826 |
. . . 4
⊢ (𝑦 = 𝑍 → (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ↔ 𝑍 ∈ trCl(𝑋, 𝐴, 𝑅))) |
22 | | eleq1 2826 |
. . . . . 6
⊢ (𝑦 = 𝑍 → (𝑦 ∈ (𝑓‘𝑖) ↔ 𝑍 ∈ (𝑓‘𝑖))) |
23 | 22 | 3anbi3d 1441 |
. . . . 5
⊢ (𝑦 = 𝑍 → ((𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)) ↔ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)))) |
24 | 23 | 3exbidv 1928 |
. . . 4
⊢ (𝑦 = 𝑍 → (∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)) ↔ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)))) |
25 | 21, 24 | imbi12d 345 |
. . 3
⊢ (𝑦 = 𝑍 → ((𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) ↔ (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖))))) |
26 | | bnj981.1 |
. . . 4
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
27 | | bnj981.3 |
. . . 4
⊢ 𝐷 = (ω ∖
{∅}) |
28 | | bnj981.4 |
. . . 4
⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} |
29 | 26, 2, 27, 28, 11 | bnj917 32900 |
. . 3
⊢ (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) |
30 | 20, 25, 29 | vtoclg1f 3502 |
. 2
⊢ (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)))) |
31 | 30 | pm2.43i 52 |
1
⊢ (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖))) |