| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | biid 261 | . 2
⊢ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) | 
| 2 |  | biid 261 | . 2
⊢
(∀𝑖 ∈
ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | 
| 3 |  | biid 261 | . 2
⊢ ((𝑛 ∈ (ω ∖
{∅}) ∧ 𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ (𝑛 ∈ (ω ∖ {∅}) ∧
𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) | 
| 4 |  | biid 261 | . 2
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅)) ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅))) | 
| 5 |  | biid 261 | . 2
⊢ ((𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) | 
| 6 |  | biid 261 | . 2
⊢ ((𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)) ↔ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖))) | 
| 7 |  | biid 261 | . 2
⊢
([𝑝 / 𝑛](𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ↔ [𝑝 / 𝑛](𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) | 
| 8 |  | biid 261 | . 2
⊢
([𝑝 / 𝑛]∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ [𝑝 / 𝑛]∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | 
| 9 |  | biid 261 | . 2
⊢
([𝑝 / 𝑛](𝑛 ∈ (ω ∖ {∅}) ∧
𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ [𝑝 / 𝑛](𝑛 ∈ (ω ∖ {∅}) ∧
𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) | 
| 10 |  | biid 261 | . 2
⊢
([(𝑓 ∪
{〈𝑛, ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)〉}) / 𝑓][𝑝 / 𝑛](𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ↔ [(𝑓 ∪ {〈𝑛, ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)〉}) / 𝑓][𝑝 / 𝑛](𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) | 
| 11 |  | biid 261 | . 2
⊢
([(𝑓 ∪
{〈𝑛, ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)〉}) / 𝑓][𝑝 / 𝑛]∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ [(𝑓 ∪ {〈𝑛, ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)〉}) / 𝑓][𝑝 / 𝑛]∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) | 
| 12 |  | biid 261 | . 2
⊢
([(𝑓 ∪
{〈𝑛, ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)〉}) / 𝑓][𝑝 / 𝑛](𝑛 ∈ (ω ∖ {∅}) ∧
𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ [(𝑓 ∪ {〈𝑛, ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)〉}) / 𝑓][𝑝 / 𝑛](𝑛 ∈ (ω ∖ {∅}) ∧
𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) | 
| 13 |  | eqid 2737 | . 2
⊢ (ω
∖ {∅}) = (ω ∖ {∅}) | 
| 14 |  | eqid 2737 | . 2
⊢ {𝑓 ∣ ∃𝑛 ∈ (ω ∖
{∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))} = {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))} | 
| 15 |  | eqid 2737 | . 2
⊢ ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) | 
| 16 |  | eqid 2737 | . 2
⊢ (𝑓 ∪ {〈𝑛, ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)〉}) = (𝑓 ∪ {〈𝑛, ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)〉}) | 
| 17 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16 | bnj907 34981 | 1
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo( trCl(𝑋, 𝐴, 𝑅), 𝐴, 𝑅)) |