Proof of Theorem bnj981
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfv 1913 | . . . 4
⊢
Ⅎ𝑦 𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) | 
| 2 |  | bnj981.2 | . . . . . . . . . . . 12
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | 
| 3 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦ω | 
| 4 |  | nfv 1913 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 suc 𝑖 ∈ 𝑛 | 
| 5 |  | nfiu1 5026 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) | 
| 6 | 5 | nfeq2 2922 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) | 
| 7 | 4, 6 | nfim 1895 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦(suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) | 
| 8 | 3, 7 | nfralw 3310 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) | 
| 9 | 2, 8 | nfxfr 1852 | . . . . . . . . . . 11
⊢
Ⅎ𝑦𝜓 | 
| 10 | 9 | nf5ri 2194 | . . . . . . . . . 10
⊢ (𝜓 → ∀𝑦𝜓) | 
| 11 |  | bnj981.5 | . . . . . . . . . 10
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) | 
| 12 | 10, 11 | bnj1096 34797 | . . . . . . . . 9
⊢ (𝜒 → ∀𝑦𝜒) | 
| 13 | 12 | nf5i 2145 | . . . . . . . 8
⊢
Ⅎ𝑦𝜒 | 
| 14 |  | nfv 1913 | . . . . . . . 8
⊢
Ⅎ𝑦 𝑖 ∈ 𝑛 | 
| 15 |  | nfv 1913 | . . . . . . . 8
⊢
Ⅎ𝑦 𝑍 ∈ (𝑓‘𝑖) | 
| 16 | 13, 14, 15 | nf3an 1900 | . . . . . . 7
⊢
Ⅎ𝑦(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)) | 
| 17 | 16 | nfex 2323 | . . . . . 6
⊢
Ⅎ𝑦∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)) | 
| 18 | 17 | nfex 2323 | . . . . 5
⊢
Ⅎ𝑦∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)) | 
| 19 | 18 | nfex 2323 | . . . 4
⊢
Ⅎ𝑦∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)) | 
| 20 | 1, 19 | nfim 1895 | . . 3
⊢
Ⅎ𝑦(𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖))) | 
| 21 |  | eleq1 2828 | . . . 4
⊢ (𝑦 = 𝑍 → (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ↔ 𝑍 ∈ trCl(𝑋, 𝐴, 𝑅))) | 
| 22 |  | eleq1 2828 | . . . . . 6
⊢ (𝑦 = 𝑍 → (𝑦 ∈ (𝑓‘𝑖) ↔ 𝑍 ∈ (𝑓‘𝑖))) | 
| 23 | 22 | 3anbi3d 1443 | . . . . 5
⊢ (𝑦 = 𝑍 → ((𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)) ↔ (𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)))) | 
| 24 | 23 | 3exbidv 1924 | . . . 4
⊢ (𝑦 = 𝑍 → (∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)) ↔ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)))) | 
| 25 | 21, 24 | imbi12d 344 | . . 3
⊢ (𝑦 = 𝑍 → ((𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) ↔ (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖))))) | 
| 26 |  | bnj981.1 | . . . 4
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) | 
| 27 |  | bnj981.3 | . . . 4
⊢ 𝐷 = (ω ∖
{∅}) | 
| 28 |  | bnj981.4 | . . . 4
⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} | 
| 29 | 26, 2, 27, 28, 11 | bnj917 34949 | . . 3
⊢ (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) | 
| 30 | 20, 25, 29 | vtoclg1f 3569 | . 2
⊢ (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)))) | 
| 31 | 30 | pm2.43i 52 | 1
⊢ (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖))) |