P. 329 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32801-32900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bnj852 32801*	Technical lemma for bnj69 32890. 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 32802*	Technical lemma for bnj69 32890. 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 32803*	Technical lemma for bnj69 32890. 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 32804*	Technical lemma for bnj69 32890. 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 32805*	Technical lemma for bnj69 32890. 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 32806*	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 32807	Equality theorem for transitive closure. (Contributed by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ (𝑋 = 𝑌 → trCl(𝑋, 𝐴, 𝑅) = trCl(𝑌, 𝐴, 𝑅))
Theorem	bnj893 32808	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 32809*	Technical lemma for bnj69 32890. 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 32810	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
Theorem	bnj908 32811*	Technical lemma for bnj69 32890. 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 32812*	Technical lemma for bnj69 32890. 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 32813*	Technical lemma for bnj69 32890. 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 32814*	Technical lemma for bnj69 32890. 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 32815*	Technical lemma for bnj69 32890. 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 32816*	Technical lemma for bnj69 32890. 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 32817*	Technical lemma for bnj69 32890. 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 32818*	Technical lemma for bnj69 32890. 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 32819	Technical lemma for bnj69 32890. 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 32820*	Technical lemma for bnj69 32890. 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 32821*	Technical lemma for bnj852 32801. 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 32822*	Technical lemma for bnj852 32801. 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 32823*	Technical lemma for bnj69 32890. 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 32824*	Technical lemma for bnj69 32890. 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 32825*	Technical lemma for bnj69 32890. 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 32826*	Technical lemma for bnj69 32890. 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 32827	Technical lemma for bnj69 32890. 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 32828*	Technical lemma for bnj69 32890. 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 32829*	Technical lemma for bnj69 32890. 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 32830*	Technical lemma for bnj69 32890. 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 32831*	Technical lemma for bnj69 32890. 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 32832	Technical lemma for bnj69 32890. 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 32833*	Version of bnj985 32834 with an additional disjoint variable condition, not requiring ax-13 2372. (Contributed by Gino Giotto, 27-Mar-2024.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′)    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ (𝐺 ∈ 𝐵 ↔ ∃𝑝𝜒″)
Theorem	bnj985 32834*	Technical lemma for bnj69 32890. 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 32833 for a version with more disjoint variable conditions, not requiring ax-13 2372. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′)    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ (𝐺 ∈ 𝐵 ↔ ∃𝑝𝜒″)
Theorem	bnj986 32835*	Technical lemma for bnj69 32890. 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 32836*	Technical lemma for bnj69 32890. 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 32837*	Technical lemma for bnj69 32890. 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 32838*	Technical lemma for bnj69 32890. 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 𝑖))
Theorem	bnj1001 32839	Technical lemma for bnj69 32890. 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 𝑖 ∈ 𝑝))
Theorem	bnj1006 32840*	Technical lemma for bnj69 32890. 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 𝑛))    &   ⊢ (𝜂 ↔ (𝑖 ∈ 𝑛 ∧ 𝑦 ∈ (𝑓‘𝑖)))    &   ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′)    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → (𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝))    ⇒   ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → pred(𝑦, 𝐴, 𝑅) ⊆ (𝐺‘suc 𝑖))
Theorem	bnj1014 32841*	Technical lemma for bnj69 32890. 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 𝑛 ∧ 𝜑 ∧ 𝜓)}    ⇒   ⊢ ((𝑔 ∈ 𝐵 ∧ 𝑗 ∈ dom 𝑔) → (𝑔‘𝑗) ⊆ trCl(𝑋, 𝐴, 𝑅))
Theorem	bnj1015 32842*	Technical lemma for bnj69 32890. 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 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ 𝐺 ∈ 𝑉    &   ⊢ 𝐽 ∈ 𝑉    ⇒   ⊢ ((𝐺 ∈ 𝐵 ∧ 𝐽 ∈ dom 𝐺) → (𝐺‘𝐽) ⊆ trCl(𝑋, 𝐴, 𝑅))
Theorem	bnj1018g 32843*	Version of bnj1018 32844 with less disjoint variable conditions, but requiring ax-13 2372. (Contributed by Gino Giotto, 27-Mar-2024.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛))    &   ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′)    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ (𝜒″ ↔ (𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″))    &   ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → 𝜒″)    &   ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → (𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝))    ⇒   ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏) → (𝐺‘suc 𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅))
Theorem	bnj1018 32844*	Technical lemma for bnj69 32890. 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 bnj1018g 32843 for a less restrictive version requiring ax-13 2372. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜏 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛))    &   ⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′)    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐵 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ (𝜒″ ↔ (𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″))    &   ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → 𝜒″)    &   ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂) → (𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝))    ⇒   ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏) → (𝐺‘suc 𝑖) ⊆ trCl(𝑋, 𝐴, 𝑅))
Theorem	bnj1020 32845*	Technical lemma for bnj69 32890. 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(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    &   ⊢ (𝜒″ ↔ (𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″))    ⇒   ⊢ ((𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃𝑝𝜏) → pred(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
Theorem	bnj1021 32846*	Technical lemma for bnj69 32890. 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	bnj907 32847*	Technical lemma for bnj69 32890. 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(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑛, 𝐶⟩})    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo( trCl(𝑋, 𝐴, 𝑅), 𝐴, 𝑅))
Theorem	bnj1029 32848	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo( trCl(𝑋, 𝐴, 𝑅), 𝐴, 𝑅))
Theorem	bnj1033 32849*	Technical lemma for bnj69 32890. 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 𝐴 ∧ 𝑋 ∈ 𝐴))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    &   ⊢ (𝜂 ↔ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)    ⇒   ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
Theorem	bnj1034 32850*	Technical lemma for bnj69 32890. 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 𝐴 ∧ 𝑋 ∈ 𝐴))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    &   ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (∃𝑓∃𝑛∃𝑖(𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)    ⇒   ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
Theorem	bnj1039 32851	Technical lemma for bnj69 32890. 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	bnj1040 32852*	Technical lemma for bnj69 32890. 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	bnj1047 32853	Technical lemma for bnj69 32890. 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 𝑖 → [𝑗 / 𝑖]𝜂))    &   ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂)    ⇒   ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → 𝜂′))
Theorem	bnj1049 32854	Technical lemma for bnj69 32890. 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	bnj1052 32855*	Technical lemma for bnj69 32890. 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 𝐴 ∧ 𝑋 ∈ 𝐴))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    &   ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (𝜂 ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))    &   ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂))    &   ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ( E Fr 𝑛 ∧ ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂)))    ⇒   ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
Theorem	bnj1053 32856*	Technical lemma for bnj69 32890. 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 𝐴 ∧ 𝑋 ∈ 𝐴))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    &   ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (𝜂 ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))    &   ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂))    &   ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂))    ⇒   ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
Theorem	bnj1071 32857	Technical lemma for bnj69 32890. 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 Fr 𝑛)
Theorem	bnj1083 32858	Technical lemma for bnj69 32890. 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	bnj1090 32859*	Technical lemma for bnj69 32890. 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.)
⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))    &   ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂))    &   ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂)    &   ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))    &   ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓))    &   ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵))    ⇒   ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂))
Theorem	bnj1093 32860*	Technical lemma for bnj69 32890. 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.)
⊢ ∃𝑗(((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0) → (𝑓‘𝑖) ⊆ 𝐵)    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    ⇒   ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵))
Theorem	bnj1097 32861	Technical lemma for bnj69 32890. 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 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    ⇒   ⊢ ((𝑖 = ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓‘𝑖) ⊆ 𝐵)
Theorem	bnj1110 32862*	Technical lemma for bnj69 32890. 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 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))    &   ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓))    &   ⊢ (𝜂′ ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵))    ⇒   ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ (𝑓‘𝑗) ⊆ 𝐵))
Theorem	bnj1112 32863*	Technical lemma for bnj69 32890. 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	bnj1118 32864*	Technical lemma for bnj69 32890. 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 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))    &   ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓))    &   ⊢ (𝜂′ ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵))    ⇒   ⊢ ∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓‘𝑖) ⊆ 𝐵)
Theorem	bnj1121 32865	Technical lemma for bnj69 32890. 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 𝐴 ∧ 𝑋 ∈ 𝐴))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    &   ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))    &   ⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))    &   ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 𝜂)    &   ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    ⇒   ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵)
Theorem	bnj1123 32866*	Technical lemma for bnj69 32890. 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 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))    &   ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂)    ⇒   ⊢ (𝜂′ ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵))
Theorem	bnj1030 32867*	Technical lemma for bnj69 32890. 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 𝐴 ∧ 𝑋 ∈ 𝐴))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    &   ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}    &   ⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))    &   ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂))    &   ⊢ (𝜑′ ↔ [𝑗 / 𝑖]𝜑)    &   ⊢ (𝜓′ ↔ [𝑗 / 𝑖]𝜓)    &   ⊢ (𝜒′ ↔ [𝑗 / 𝑖]𝜒)    &   ⊢ (𝜃′ ↔ [𝑗 / 𝑖]𝜃)    &   ⊢ (𝜏′ ↔ [𝑗 / 𝑖]𝜏)    &   ⊢ (𝜁′ ↔ [𝑗 / 𝑖]𝜁)    &   ⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂)    &   ⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′))    &   ⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓))    ⇒   ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
Theorem	bnj1124 32868	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    ⇒   ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
Theorem	bnj1133 32869*	Technical lemma for bnj69 32890. 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 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜏 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜃))    &   ⊢ ((𝑖 ∈ 𝑛 ∧ 𝜏) → 𝜃)    ⇒   ⊢ (𝜒 → ∀𝑖 ∈ 𝑛 𝜃)
Theorem	bnj1128 32870*	Technical lemma for bnj69 32890. 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 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜃 ↔ (𝜒 → (𝑓‘𝑖) ⊆ 𝐴))    &   ⊢ (𝜏 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜃))    &   ⊢ (𝜑′ ↔ [𝑗 / 𝑖]𝜑)    &   ⊢ (𝜓′ ↔ [𝑗 / 𝑖]𝜓)    &   ⊢ (𝜒′ ↔ [𝑗 / 𝑖]𝜒)    &   ⊢ (𝜃′ ↔ [𝑗 / 𝑖]𝜃)    ⇒   ⊢ (𝑌 ∈ trCl(𝑋, 𝐴, 𝑅) → 𝑌 ∈ 𝐴)
Theorem	bnj1127 32871	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑌 ∈ trCl(𝑋, 𝐴, 𝑅) → 𝑌 ∈ 𝐴)
Theorem	bnj1125 32872	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl(𝑋, 𝐴, 𝑅)) → trCl(𝑌, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
Theorem	bnj1145 32873*	Technical lemma for bnj69 32890. 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 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜃 ↔ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝜒) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)))    ⇒   ⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴
Theorem	bnj1147 32874	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴
Theorem	bnj1137 32875*	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo(𝐵, 𝐴, 𝑅))
Theorem	bnj1148 32876	Property of pred. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ∈ V)
Theorem	bnj1136 32877*	Technical lemma for bnj69 32890. 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(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))    &   ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)
Theorem	bnj1152 32878	Technical lemma for bnj69 32890. 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	bnj1154 32879*	Property of Fr. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ∧ 𝐵 ∈ V) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
Theorem	bnj1171 32880	Technical lemma for bnj69 32890. 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	bnj1172 32881	Technical lemma for bnj69 32890. 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.)
⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵)    &   ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵))))    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (𝜃 ↔ 𝑤 ∈ 𝐴))    ⇒   ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐴 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵))))
Theorem	bnj1173 32882	Technical lemma for bnj69 32890. 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.)
⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵)    &   ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑅 FrSe 𝐴)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (𝜃 ↔ 𝑤 ∈ 𝐴))
Theorem	bnj1174 32883	Technical lemma for bnj69 32890. 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.)
⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵)    &   ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))    &   ⊢ (𝜃 → (𝑤𝑅𝑧 → 𝑤 ∈ trCl(𝑋, 𝐴, 𝑅)))    ⇒   ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵))))
Theorem	bnj1175 32884	Technical lemma for bnj69 32890. 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.)
⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵)    &   ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧)))    &   ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴))    ⇒   ⊢ (𝜃 → (𝑤𝑅𝑧 → 𝑤 ∈ trCl(𝑋, 𝐴, 𝑅)))
Theorem	bnj1176 32885*	Technical lemma for bnj69 32890. 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.)
⊢ ((𝜑 ∧ 𝜓) → (𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V))    &   ⊢ ((𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V) → ∃𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧)    ⇒   ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
Theorem	bnj1177 32886	Technical lemma for bnj69 32890. 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.)
⊢ (𝜓 ↔ (𝑋 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑋))    &   ⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑅 FrSe 𝐴)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐵 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V))
Theorem	bnj1186 32887*	Technical lemma for bnj69 32890. 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	bnj1190 32888*	Technical lemma for bnj69 32890. 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 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅))    &   ⊢ (𝜓 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∃𝑤 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝑤)
Theorem	bnj1189 32889*	Technical lemma for bnj69 32890. 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 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅))    &   ⊢ (𝜓 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥))    &   ⊢ (𝜒 ↔ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
20.4.3  The existence of a minimal element in certain classes
Theorem	bnj69 32890*	Existence of a minimal element in certain classes: if 𝑅 is well-founded and set-like on 𝐴, then every nonempty subclass of 𝐴 has a minimal element. 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.)
⊢ ((𝑅 FrSe 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
Theorem	bnj1228 32891*	Existence of a minimal element in certain classes: if 𝑅 is well-founded and set-like on 𝐴, then every nonempty subclass of 𝐴 has a minimal element. 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.)
⊢ (𝑤 ∈ 𝐵 → ∀𝑥 𝑤 ∈ 𝐵)    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
20.4.4  Well-founded induction
Theorem	bnj1204 32892*	Well-founded induction. 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.)
⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	bnj1234 32893*	Technical lemma for bnj60 32942. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝑍 = ⟨𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝐷 = {𝑔 ∣ ∃𝑑 ∈ 𝐵 (𝑔 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘𝑍))}    ⇒   ⊢ 𝐶 = 𝐷
Theorem	bnj1245 32894*	Technical lemma for bnj60 32942. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐷 = (dom 𝑔 ∩ dom ℎ)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)}    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷)))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥))    &   ⊢ 𝑍 = ⟨𝑥, (ℎ ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝐾 = {ℎ ∣ ∃𝑑 ∈ 𝐵 (ℎ Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (ℎ‘𝑥) = (𝐺‘𝑍))}    ⇒   ⊢ (𝜑 → dom ℎ ⊆ 𝐴)
Theorem	bnj1256 32895*	Technical lemma for bnj60 32942. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐷 = (dom 𝑔 ∩ dom ℎ)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)}    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷)))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 𝑔 Fn 𝑑)
Theorem	bnj1259 32896*	Technical lemma for bnj60 32942. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐷 = (dom 𝑔 ∩ dom ℎ)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)}    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷)))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 ℎ Fn 𝑑)
Theorem	bnj1253 32897*	Technical lemma for bnj60 32942. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐷 = (dom 𝑔 ∩ dom ℎ)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)}    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷)))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥))    ⇒   ⊢ (𝜑 → 𝐸 ≠ ∅)
Theorem	bnj1279 32898*	Technical lemma for bnj60 32942. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐷 = (dom 𝑔 ∩ dom ℎ)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)}    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷)))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥))    ⇒   ⊢ ((𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥) → ( pred(𝑥, 𝐴, 𝑅) ∩ 𝐸) = ∅)
Theorem	bnj1286 32899*	Technical lemma for bnj60 32942. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐷 = (dom 𝑔 ∩ dom ℎ)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)}    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷)))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥))    ⇒   ⊢ (𝜓 → pred(𝑥, 𝐴, 𝑅) ⊆ 𝐷)
Theorem	bnj1280 32900*	Technical lemma for bnj60 32942. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐷 = (dom 𝑔 ∩ dom ℎ)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)}    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷)))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜓 → ( pred(𝑥, 𝐴, 𝑅) ∩ 𝐸) = ∅)    ⇒   ⊢ (𝜓 → (𝑔 ↾ pred(𝑥, 𝐴, 𝑅)) = (ℎ ↾ pred(𝑥, 𝐴, 𝑅)))