Proof of Theorem bnj999
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bnj999.3 | . . . . . . 7
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) | 
| 2 |  | bnj999.7 | . . . . . . 7
⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑) | 
| 3 |  | bnj999.8 | . . . . . . 7
⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓) | 
| 4 |  | bnj999.9 | . . . . . . 7
⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) | 
| 5 |  | vex 3484 | . . . . . . 7
⊢ 𝑝 ∈ V | 
| 6 | 1, 2, 3, 4, 5 | bnj919 34781 | . . . . . 6
⊢ (𝜒′ ↔ (𝑝 ∈ 𝐷 ∧ 𝑓 Fn 𝑝 ∧ 𝜑′ ∧ 𝜓′)) | 
| 7 |  | bnj999.10 | . . . . . 6
⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′) | 
| 8 |  | bnj999.11 | . . . . . 6
⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′) | 
| 9 |  | bnj999.12 | . . . . . 6
⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) | 
| 10 |  | bnj999.16 | . . . . . . 7
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) | 
| 11 | 10 | bnj918 34780 | . . . . . 6
⊢ 𝐺 ∈ V | 
| 12 | 6, 7, 8, 9, 11 | bnj976 34791 | . . . . 5
⊢ (𝜒″ ↔ (𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″)) | 
| 13 | 12 | bnj1254 34823 | . . . 4
⊢ (𝜒″ → 𝜓″) | 
| 14 | 13 | anim1i 615 | . . 3
⊢ ((𝜒″ ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖))) → (𝜓″ ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)))) | 
| 15 |  | bnj252 34717 | . . 3
⊢ ((𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) ↔ (𝜒″ ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)))) | 
| 16 |  | bnj252 34717 | . . 3
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) ↔ (𝜓″ ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)))) | 
| 17 | 14, 15, 16 | 3imtr4i 292 | . 2
⊢ ((𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → (𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖))) | 
| 18 |  | ssiun2 5047 | . . . 4
⊢ (𝑦 ∈ (𝐺‘𝑖) → pred(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) | 
| 19 | 18 | bnj708 34770 | . . 3
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → pred(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) | 
| 20 |  | 3simpa 1149 | . . . . . 6
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝) → (𝜓″ ∧ 𝑖 ∈ ω)) | 
| 21 | 20 | ancomd 461 | . . . . 5
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝) → (𝑖 ∈ ω ∧ 𝜓″)) | 
| 22 |  | simp3 1139 | . . . . 5
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝) → suc 𝑖 ∈ 𝑝) | 
| 23 |  | bnj999.2 | . . . . . . . 8
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | 
| 24 | 23, 3, 5 | bnj539 34905 | . . . . . . 7
⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑝 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | 
| 25 |  | bnj999.15 | . . . . . . 7
⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) | 
| 26 | 24, 8, 25, 10 | bnj965 34956 | . . . . . 6
⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑝 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) | 
| 27 | 26 | bnj228 34749 | . . . . 5
⊢ ((𝑖 ∈ ω ∧ 𝜓″) → (suc 𝑖 ∈ 𝑝 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) | 
| 28 | 21, 22, 27 | sylc 65 | . . . 4
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) | 
| 29 | 28 | bnj721 34771 | . . 3
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) | 
| 30 | 19, 29 | sseqtrrd 4021 | . 2
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → pred(𝑦, 𝐴, 𝑅) ⊆ (𝐺‘suc 𝑖)) | 
| 31 | 17, 30 | syl 17 | 1
⊢ ((𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → pred(𝑦, 𝐴, 𝑅) ⊆ (𝐺‘suc 𝑖)) |