P. 351 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35001-35100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bnj157 35001*	Well-founded induction restricted to a set (𝐴 ∈ V). The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝑅 Fr 𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	bnj66 35002*	Technical lemma for bnj60 35204. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)}    &   ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    ⇒   ⊢ (𝑔 ∈ 𝐶 → Rel 𝑔)
Theorem	bnj91 35003*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ ([𝑍 / 𝑦]𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj92 35004*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ ([𝑍 / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑍 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj93 35005*	Technical lemma for bnj97 35008. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → pred(𝑥, 𝐴, 𝑅) ∈ V)
Theorem	bnj95 35006	Technical lemma for bnj124 35013. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ 𝐹 ∈ V
Theorem	bnj96 35007*	Technical lemma for bnj150 35018. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → dom 𝐹 = 1o)
Theorem	bnj97 35008*	Technical lemma for bnj150 35018. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj98 35009	Technical lemma for bnj150 35018. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))
Theorem	bnj106 35010*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ([𝐹 / 𝑓][1o / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj118 35011*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    ⇒   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj121 35012*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁)    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓)    ⇒   ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))
Theorem	bnj124 35013*	Technical lemma for bnj150 35018. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′)    &   ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))    ⇒   ⊢ (𝜁″ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1o ∧ 𝜑″ ∧ 𝜓″)))
Theorem	bnj125 35014*	Technical lemma for bnj150 35018. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ (𝜑″ ↔ (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj126 35015*	Technical lemma for bnj150 35018. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj130 35016*	Technical lemma for bnj151 35019. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓)    &   ⊢ (𝜃′ ↔ [1o / 𝑛]𝜃)    ⇒   ⊢ (𝜃′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))
Theorem	bnj149 35017*	Technical lemma for bnj151 35019. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ (𝜃1 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜁0 ↔ (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0)    &   ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′)    &   ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′)    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    ⇒   ⊢ 𝜃1
Theorem	bnj150 35018*	Technical lemma for bnj151 35019. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓)    &   ⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′)    ⇒   ⊢ 𝜃0
Theorem	bnj151 35019*	Technical lemma for bnj153 35022. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜏 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜃))    &   ⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓)    &   ⊢ (𝜃′ ↔ [1o / 𝑛]𝜃)    &   ⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜃1 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′)    &   ⊢ (𝜁0 ↔ (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0)    &   ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′)    &   ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′)    ⇒   ⊢ (𝑛 = 1o → ((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃))
Theorem	bnj154 35020*	Technical lemma for bnj153 35022. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′)    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    ⇒   ⊢ (𝜑1 ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj155 35021*	Technical lemma for bnj153 35022. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′)    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ (𝜓1 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj153 35022*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜏 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜃))    ⇒   ⊢ (𝑛 = 1o → ((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃))
Theorem	bnj207 35023*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑀 / 𝑛]𝜒)    &   ⊢ 𝑀 ∈ V    ⇒   ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑀 ∧ 𝜑′ ∧ 𝜓′)))
Theorem	bnj213 35024	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
Theorem	bnj222 35025*	Technical lemma for bnj229 35026. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ (𝜓 ↔ ∀𝑚 ∈ ω (suc 𝑚 ∈ 𝑁 → (𝐹‘suc 𝑚) = ∪ 𝑦 ∈ (𝐹‘𝑚) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj229 35026*	Technical lemma for bnj517 35027. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑛 ∈ 𝑁 ∧ (suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓)) → (𝐹‘𝑛) ⊆ 𝐴)
Theorem	bnj517 35027*	Technical lemma for bnj518 35028. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) → ∀𝑛 ∈ 𝑁 (𝐹‘𝑛) ⊆ 𝐴)
Theorem	bnj518 35028*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜏 ↔ (𝜑 ∧ 𝜓 ∧ 𝑛 ∈ ω ∧ 𝑝 ∈ 𝑛))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏) → ∀𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V)
Theorem	bnj523 35029*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑)    &   ⊢ 𝑀 ∈ V    ⇒   ⊢ (𝜑′ ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅))
Theorem	bnj526 35030*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑋, 𝐴, 𝑅))
Theorem	bnj528 35031	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    ⇒   ⊢ 𝐺 ∈ V
Theorem	bnj535 35032*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝑛 = (𝑚 ∪ {𝑚}) ∧ 𝑓 Fn 𝑚) → 𝐺 Fn 𝑛)
Theorem	bnj539 35033*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓)    &   ⊢ 𝑀 ∈ V    ⇒   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑀 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj540 35034*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj543 35035*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)
Theorem	bnj544 35036*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)
Theorem	bnj545 35037	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    &   ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝜑″)
Theorem	bnj546 35038*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V)
Theorem	bnj548 35039*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) ∧ 𝑖 ∈ 𝑚) → 𝐵 = 𝐾)
Theorem	bnj553 35040*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖) → (𝐺‘𝑚) = 𝐿)
Theorem	bnj554 35041*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    ⇒   ⊢ ((𝜂 ∧ 𝜁) → ((𝐺‘𝑚) = 𝐿 ↔ (𝐺‘suc 𝑖) = 𝐾))
Theorem	bnj556 35042	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    ⇒   ⊢ (𝜂 → 𝜎)
Theorem	bnj557 35043*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁) → (𝐺‘𝑚) = 𝐿)
Theorem	bnj558 35044*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁) → (𝐺‘suc 𝑖) = 𝐾)
Theorem	bnj561 35045	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛)
Theorem	bnj562 35046	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝜑″)    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″)
Theorem	bnj570 35047*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖))    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛)    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌) → (𝐺‘suc 𝑖) = 𝐾)
Theorem	bnj571 35048*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    &   ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛)    &   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″)
Theorem	bnj605 35049*	Technical lemma. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))    &   ⊢ (𝜑″ ↔ [𝑓 / 𝑓]𝜑)    &   ⊢ (𝜓″ ↔ [𝑓 / 𝑓]𝜓)    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ 𝑓 ∈ V    &   ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜑″ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚∃𝑝𝜂)    &   ⊢ ((𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛) → 𝜒′)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝑓 Fn 𝑛)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″)    ⇒   ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
Theorem	bnj581 35050*	Technical lemma for bnj580 35055. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Remove unnecessary distinct variable conditions. (Revised by Andrew Salmon, 9-Jul-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)    &   ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)    &   ⊢ (𝜒′ ↔ [𝑔 / 𝑓]𝜒)    ⇒   ⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
Theorem	bnj589 35051*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑓‘suc 𝑘) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj590 35052	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝐵 = suc 𝑖 ∧ 𝜓) → (𝑖 ∈ ω → (𝐵 ∈ 𝑛 → (𝑓‘𝐵) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))))
Theorem	bnj591 35053*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))    ⇒   ⊢ ([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)))
Theorem	bnj594 35054*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))    &   ⊢ ([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)))    &   ⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))    ⇒   ⊢ ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)
Theorem	bnj580 35055*	Technical lemma for bnj579 35056. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)    &   ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)    &   ⊢ (𝜒′ ↔ [𝑔 / 𝑓]𝜒)    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))    &   ⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))    ⇒   ⊢ (𝑛 ∈ 𝐷 → ∃*𝑓𝜒)
Theorem	bnj579 35056*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ (𝑛 ∈ 𝐷 → ∃*𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
Theorem	bnj602 35057	Equality theorem for the pred function constant. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑋 = 𝑌 → pred(𝑋, 𝐴, 𝑅) = pred(𝑌, 𝐴, 𝑅))
Theorem	bnj607 35058*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ 𝐺 ∈ V    &   ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚∃𝑝𝜂)    &   ⊢ ((𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛) → 𝜒′)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″)    &   ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜑0 ↔ [ℎ / 𝑓]𝜑)    &   ⊢ (𝜓0 ↔ [ℎ / 𝑓]𝜓)    &   ⊢ (𝜑1 ↔ [𝐺 / ℎ]𝜑0)    &   ⊢ (𝜓1 ↔ [𝐺 / ℎ]𝜓0)    ⇒   ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
Theorem	bnj609 35059*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑋, 𝐴, 𝑅))
Theorem	bnj611 35060*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj600 35061*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))    &   ⊢ (𝜑′ ↔ [𝑚 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑚 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑚 / 𝑛]𝜒)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    ⇒   ⊢ (𝑛 ≠ 1o → ((𝑛 ∈ 𝐷 ∧ 𝜃) → 𝜒))
Theorem	bnj601 35062*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))    ⇒   ⊢ (𝑛 ≠ 1o → ((𝑛 ∈ 𝐷 ∧ 𝜃) → 𝜒))
Theorem	bnj852 35063*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛 ∈ 𝐷 ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
Theorem	bnj864 35064*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷))    &   ⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    ⇒   ⊢ (𝜒 → ∃!𝑓𝜃)
Theorem	bnj865 35065*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷))    &   ⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    ⇒   ⊢ ∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)
Theorem	bnj873 35066*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)    &   ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)    ⇒   ⊢ 𝐵 = {𝑔 ∣ ∃𝑛 ∈ 𝐷 (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′)}
Theorem	bnj849 35067*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷))    &   ⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)    &   ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)    &   ⊢ (𝜃′ ↔ [𝑔 / 𝑓]𝜃)    &   ⊢ (𝜏 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)
Theorem	bnj882 35068*	Definition (using hypotheses for readability) of the function giving the transitive closure of 𝑋 in 𝐴 by 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    ⇒   ⊢ trCl(𝑋, 𝐴, 𝑅) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓(𝑓‘𝑖)
Theorem	bnj18eq1 35069	Equality theorem for transitive closure. (Contributed by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ (𝑋 = 𝑌 → trCl(𝑋, 𝐴, 𝑅) = trCl(𝑌, 𝐴, 𝑅))
Theorem	bnj893 35070	Property of trCl. Under certain conditions, the transitive closure of 𝑋 in 𝐴 by 𝑅 is a set. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) ∈ V)
Theorem	bnj900 35071*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    ⇒   ⊢ (𝑓 ∈ 𝐵 → ∅ ∈ dom 𝑓)
Theorem	bnj906 35072	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
Theorem	bnj908 35073*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))    &   ⊢ (𝜑′ ↔ [𝑚 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑚 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑚 / 𝑛]𝜒)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒′ ∧ 𝜂) → ∃𝑓(𝐺 Fn 𝑛 ∧ 𝜑″ ∧ 𝜓″))
Theorem	bnj911 35074*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∀𝑖(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
Theorem	bnj916 35075*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    ⇒   ⊢ (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)))
Theorem	bnj917 35076*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    ⇒   ⊢ (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)))
Theorem	bnj934 35077*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ ((𝜑 ∧ (𝐺‘∅) = (𝑓‘∅)) → 𝜑″)
Theorem	bnj929 35078*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′)    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ∧ 𝜑) → 𝜑″)
Theorem	bnj938 35079*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝜏 ∧ 𝜎) → ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V)
Theorem	bnj944 35080*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′)    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜎 ↔ (𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛))    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝜑″)
Theorem	bnj953 35081	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝐺‘𝑖) = (𝑓‘𝑖) → ∀𝑦(𝐺‘𝑖) = (𝑓‘𝑖))    ⇒   ⊢ (((𝐺‘𝑖) = (𝑓‘𝑖) ∧ (𝐺‘suc 𝑖) = (𝑓‘suc 𝑖) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛) ∧ 𝜓) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))
Theorem	bnj958 35082*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ ((𝐺‘𝑖) = (𝑓‘𝑖) → ∀𝑦(𝐺‘𝑖) = (𝑓‘𝑖))
Theorem	bnj1000 35083*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ 𝐺 ∈ V    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj965 35084*	Technical lemma for bnj852 35063. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj964 35085*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))    &   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝜓″)
Theorem	bnj966 35086*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐶 ∈ V)    &   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐺 Fn 𝑝)    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑛 = suc 𝑖)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))
Theorem	bnj967 35087*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐶 ∈ V)    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛) ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ suc 𝑖 ∈ 𝑛)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))
Theorem	bnj969 35088*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜎 ↔ (𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛))    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝐶 ∈ V)
Theorem	bnj970 35089	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝑝 ∈ 𝐷)
Theorem	bnj910 35090*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′)    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜎 ↔ (𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ∧ 𝑚 ∈ 𝑛))    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛)) → 𝜒″)
Theorem	bnj978 35091*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜃 → 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo( trCl(𝑋, 𝐴, 𝑅), 𝐴, 𝑅))
Theorem	bnj981 35092*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    ⇒   ⊢ (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) → ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)))
Theorem	bnj983 35093*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    ⇒   ⊢ (𝑍 ∈ trCl(𝑋, 𝐴, 𝑅) ↔ ∃𝑓∃𝑛∃𝑖(𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ (𝑓‘𝑖)))
Theorem	bnj984 35094	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ 𝐵 ↔ [𝐺 / 𝑓]∃𝑛𝜒))
Theorem	bnj985v 35095*	Version of bnj985 35096 with an additional disjoint variable condition, not requiring ax-13 2376. (Contributed by GG, 27-Mar-2024.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′)    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ (𝐺 ∈ 𝐵 ↔ ∃𝑝𝜒″)
Theorem	bnj985 35096*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). See bnj985v 35095 for a version with more disjoint variable conditions, not requiring ax-13 2376. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′)    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ (𝐺 ∈ 𝐵 ↔ ∃𝑝𝜒″)
Theorem	bnj986 35097*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛))    ⇒   ⊢ (𝜒 → ∃𝑚∃𝑝𝜏)
Theorem	bnj996 35098*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛))    &   ⊢ (𝜂 ↔ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    ⇒   ⊢ ∃𝑓∃𝑛∃𝑖∃𝑚∃𝑝(𝜃 → (𝜒 ∧ 𝜏 ∧ 𝜂))
Theorem	bnj998 35099*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛))    &   ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′)    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → 𝜒″)
Theorem	bnj999 35100*	Technical lemma for bnj69 35152. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ ((𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → pred(𝑦, 𝐴, 𝑅) ⊆ (𝐺‘suc 𝑖))