P. 355 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35401-35500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bnj1175 35401	Technical lemma for bnj69 35407. 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 35402*	Technical lemma for bnj69 35407. 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 35403	Technical lemma for bnj69 35407. 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 35404*	Technical lemma for bnj69 35407. 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 35405*	Technical lemma for bnj69 35407. 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 35406*	Technical lemma for bnj69 35407. 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 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅))    &   ⊢ (𝜓 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝑅𝑥))    &   ⊢ (𝜒 ↔ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
21.4.3  The existence of a minimal element in certain classes
Theorem	bnj69 35407*	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 35408*	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 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
21.4.4  Well-founded induction
Theorem	bnj1204 35409*	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 35410*	Technical lemma for bnj60 35459. 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 35411*	Technical lemma for bnj60 35459. 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 35412*	Technical lemma for bnj60 35459. 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 35413*	Technical lemma for bnj60 35459. 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 35414*	Technical lemma for bnj60 35459. 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 35415*	Technical lemma for bnj60 35459. 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 35416*	Technical lemma for bnj60 35459. 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 35417*	Technical lemma for bnj60 35459. 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(𝑥, 𝐴, 𝑅)))
Theorem	bnj1296 35418*	Technical lemma for bnj60 35459. 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(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝐾 = {𝑔 ∣ ∃𝑑 ∈ 𝐵 (𝑔 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘𝑍))}    &   ⊢ 𝑊 = ⟨𝑥, (ℎ ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝐿 = {ℎ ∣ ∃𝑑 ∈ 𝐵 (ℎ Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (ℎ‘𝑥) = (𝐺‘𝑊))}    ⇒   ⊢ (𝜓 → (𝑔‘𝑥) = (ℎ‘𝑥))
Theorem	bnj1309 35419*	Technical lemma for bnj60 35459. 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	bnj1307 35420*	Technical lemma for bnj60 35459. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ (𝑤 ∈ 𝐵 → ∀𝑥 𝑤 ∈ 𝐵)    ⇒   ⊢ (𝑤 ∈ 𝐶 → ∀𝑥 𝑤 ∈ 𝐶)
Theorem	bnj1311 35421*	Technical lemma for bnj60 35459. 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	bnj1318 35422	Technical lemma for bnj60 35459. 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	bnj1326 35423*	Technical lemma for bnj60 35459. 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	bnj1321 35424*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ ∃𝑓𝜏) → ∃!𝑓𝜏)
Theorem	bnj1364 35425	Property of FrSe. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑅 FrSe 𝐴 → 𝑅 Se 𝐴)
Theorem	bnj1371 35426*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ (𝜏′ ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))    ⇒   ⊢ (𝑓 ∈ 𝐻 → Fun 𝑓)
Theorem	bnj1373 35427*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    ⇒   ⊢ (𝜏′ ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))
Theorem	bnj1374 35428*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    ⇒   ⊢ (𝑓 ∈ 𝐻 → 𝑓 ∈ 𝐶)
Theorem	bnj1384 35429*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    ⇒   ⊢ (𝑅 FrSe 𝐴 → Fun 𝑃)
Theorem	bnj1388 35430*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    ⇒   ⊢ (𝜒 → ∀𝑦 ∈ pred (𝑥, 𝐴, 𝑅)∃𝑓𝜏′)
Theorem	bnj1398 35431*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑥, 𝐴, 𝑅)({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))    &   ⊢ (𝜂 ↔ (𝜃 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑧 ∈ ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))    ⇒   ⊢ (𝜒 → ∪ 𝑦 ∈ pred (𝑥, 𝐴, 𝑅)({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)) = dom 𝑃)
Theorem	bnj1413 35432*	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)
Theorem	bnj1408 35433*	Technical lemma for bnj1414 35434. 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 (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))    &   ⊢ 𝐶 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))    &   ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))    &   ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)
Theorem	bnj1414 35434*	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)
Theorem	bnj1415 35435*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    ⇒   ⊢ (𝜒 → dom 𝑃 = trCl(𝑥, 𝐴, 𝑅))
Theorem	bnj1416 35436	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ (𝜒 → dom 𝑃 = trCl(𝑥, 𝐴, 𝑅))    ⇒   ⊢ (𝜒 → dom 𝑄 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))
Theorem	bnj1418 35437	Property of pred. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → 𝑦𝑅𝑥)
Theorem	bnj1417 35438*	Technical lemma for bnj60 35459. 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.)
⊢ (𝜑 ↔ 𝑅 FrSe 𝐴)    &   ⊢ (𝜓 ↔ ¬ 𝑥 ∈ trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜓))    &   ⊢ (𝜃 ↔ (𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒))    &   ⊢ 𝐵 = ( pred(𝑥, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑥, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ trCl(𝑥, 𝐴, 𝑅))
Theorem	bnj1421 35439*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ (𝜒 → Fun 𝑃)    &   ⊢ (𝜒 → dom 𝑄 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))    &   ⊢ (𝜒 → dom 𝑃 = trCl(𝑥, 𝐴, 𝑅))    ⇒   ⊢ (𝜒 → Fun 𝑄)
Theorem	bnj1444 35440*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    &   ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸))    &   ⊢ (𝜂 ↔ (𝜃 ∧ 𝑧 ∈ {𝑥}))    &   ⊢ (𝜁 ↔ (𝜃 ∧ 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)))    &   ⊢ (𝜌 ↔ (𝜁 ∧ 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓))    ⇒   ⊢ (𝜌 → ∀𝑦𝜌)
Theorem	bnj1445 35441*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    &   ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸))    &   ⊢ (𝜂 ↔ (𝜃 ∧ 𝑧 ∈ {𝑥}))    &   ⊢ (𝜁 ↔ (𝜃 ∧ 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)))    &   ⊢ (𝜌 ↔ (𝜁 ∧ 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓))    &   ⊢ (𝜎 ↔ (𝜌 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))    &   ⊢ (𝜑 ↔ (𝜎 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)))    &   ⊢ 𝑋 = ⟨𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))⟩    ⇒   ⊢ (𝜎 → ∀𝑑𝜎)
Theorem	bnj1446 35442*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    ⇒   ⊢ ((𝑄‘𝑧) = (𝐺‘𝑊) → ∀𝑑(𝑄‘𝑧) = (𝐺‘𝑊))
Theorem	bnj1447 35443*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    ⇒   ⊢ ((𝑄‘𝑧) = (𝐺‘𝑊) → ∀𝑦(𝑄‘𝑧) = (𝐺‘𝑊))
Theorem	bnj1448 35444*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    ⇒   ⊢ ((𝑄‘𝑧) = (𝐺‘𝑊) → ∀𝑓(𝑄‘𝑧) = (𝐺‘𝑊))
Theorem	bnj1449 35445*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    &   ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸))    &   ⊢ (𝜂 ↔ (𝜃 ∧ 𝑧 ∈ {𝑥}))    &   ⊢ (𝜁 ↔ (𝜃 ∧ 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)))    ⇒   ⊢ (𝜁 → ∀𝑓𝜁)
Theorem	bnj1442 35446*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    &   ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸))    &   ⊢ (𝜂 ↔ (𝜃 ∧ 𝑧 ∈ {𝑥}))    ⇒   ⊢ (𝜂 → (𝑄‘𝑧) = (𝐺‘𝑊))
Theorem	bnj1450 35447*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    &   ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸))    &   ⊢ (𝜂 ↔ (𝜃 ∧ 𝑧 ∈ {𝑥}))    &   ⊢ (𝜁 ↔ (𝜃 ∧ 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)))    &   ⊢ (𝜌 ↔ (𝜁 ∧ 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓))    &   ⊢ (𝜎 ↔ (𝜌 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))    &   ⊢ (𝜑 ↔ (𝜎 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)))    &   ⊢ 𝑋 = ⟨𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))⟩    ⇒   ⊢ (𝜁 → (𝑄‘𝑧) = (𝐺‘𝑊))
Theorem	bnj1423 35448*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    &   ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑃 Fn trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))    ⇒   ⊢ (𝜒 → ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊))
Theorem	bnj1452 35449*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    &   ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))    ⇒   ⊢ (𝜒 → 𝐸 ∈ 𝐵)
Theorem	bnj1466 35450*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    ⇒   ⊢ (𝑤 ∈ 𝑄 → ∀𝑓 𝑤 ∈ 𝑄)
Theorem	bnj1467 35451*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    ⇒   ⊢ (𝑤 ∈ 𝑄 → ∀𝑑 𝑤 ∈ 𝑄)
Theorem	bnj1463 35452*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    &   ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜒 → 𝑄 ∈ V)    &   ⊢ (𝜒 → ∀𝑧 ∈ 𝐸 (𝑄‘𝑧) = (𝐺‘𝑊))    &   ⊢ (𝜒 → 𝑄 Fn 𝐸)    &   ⊢ (𝜒 → 𝐸 ∈ 𝐵)    ⇒   ⊢ (𝜒 → 𝑄 ∈ 𝐶)
Theorem	bnj1489 35453*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    ⇒   ⊢ (𝜒 → 𝑄 ∈ V)
Theorem	bnj1491 35454*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ (𝜒 → (𝑄 ∈ 𝐶 ∧ dom 𝑄 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    ⇒   ⊢ ((𝜒 ∧ 𝑄 ∈ V) → ∃𝑓(𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))
Theorem	bnj1312 35455*	Technical lemma for bnj60 35459. 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 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏}    &   ⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥))    &   ⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏)    &   ⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}    &   ⊢ 𝑃 = ∪ 𝐻    &   ⊢ 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺‘𝑍)⟩})    &   ⊢ 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩    &   ⊢ 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))    ⇒   ⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))
Theorem	bnj1493 35456*	Technical lemma for bnj60 35459. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    ⇒   ⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑓 ∈ 𝐶 dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))
Theorem	bnj1497 35457*	Technical lemma for bnj60 35459. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    ⇒   ⊢ ∀𝑔 ∈ 𝐶 Fun 𝑔
Theorem	bnj1498 35458*	Technical lemma for bnj60 35459. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐹 = ∪ 𝐶    ⇒   ⊢ (𝑅 FrSe 𝐴 → dom 𝐹 = 𝐴)
21.4.5  Well-founded recursion, part 1 of 3
Theorem	bnj60 35459*	Well-founded recursion, part 1 of 3. 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.)
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)}    &   ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐹 = ∪ 𝐶    ⇒   ⊢ (𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴)
Theorem	bnj1514 35460*	Technical lemma for bnj1500 35465. 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 𝑓(𝑓‘𝑥) = (𝐺‘𝑌))
Theorem	bnj1518 35461*	Technical lemma for bnj1500 35465. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐹 = ∪ 𝐶    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝑓 ∈ 𝐶 ∧ 𝑥 ∈ dom 𝑓))    ⇒   ⊢ (𝜓 → ∀𝑑𝜓)
Theorem	bnj1519 35462*	Technical lemma for bnj1500 35465. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐹 = ∪ 𝐶    ⇒   ⊢ ((𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩) → ∀𝑑(𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩))
Theorem	bnj1520 35463*	Technical lemma for bnj1500 35465. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐹 = ∪ 𝐶    ⇒   ⊢ ((𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩) → ∀𝑓(𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩))
Theorem	bnj1501 35464*	Technical lemma for bnj1500 35465. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐹 = ∪ 𝐶    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝑓 ∈ 𝐶 ∧ 𝑥 ∈ dom 𝑓))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑))    ⇒   ⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩))
21.4.6  Well-founded recursion, part 2 of 3
Theorem	bnj1500 35465*	Well-founded recursion, part 2 of 3. 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.)
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)}    &   ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐹 = ∪ 𝐶    ⇒   ⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩))
Theorem	bnj1525 35466*	Technical lemma for bnj1522 35469. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐹 = ∪ 𝐶    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘⟨𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))⟩)))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝐹 ≠ 𝐻))    ⇒   ⊢ (𝜓 → ∀𝑥𝜓)
Theorem	bnj1529 35467*	Technical lemma for bnj1522 35469. 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(𝑦, 𝐴, 𝑅))⟩))
Theorem	bnj1523 35468*	Technical lemma for bnj1522 35469. 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 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐹 = ∪ 𝐶    &   ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘⟨𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))⟩)))    &   ⊢ (𝜓 ↔ (𝜑 ∧ 𝐹 ≠ 𝐻))    &   ⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ (𝐻‘𝑥)))    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐻‘𝑥)}    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑦 ∈ 𝐷 ∧ ∀𝑧 ∈ 𝐷 ¬ 𝑧𝑅𝑦))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘⟨𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) → 𝐹 = 𝐻)
21.4.7  Well-founded recursion, part 3 of 3
Theorem	bnj1522 35469*	Well-founded recursion, part 3 of 3. 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.)
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)}    &   ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    &   ⊢ 𝐹 = ∪ 𝐶    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘⟨𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) → 𝐹 = 𝐻)
21.5  Mathbox for BTernaryTau
21.5.1  First-order logic
21.5.1.1  Auxiliary axiom schemes
Theorem	nfan1c 35470	Variant of nfan 1928 and commuted form of nfan1 2235. (Contributed by BTernaryTau, 31-Jul-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ Ⅎ𝑥(𝜓 ∧ 𝜑)
Theorem	cbvex1v 35471*	Rule used to change bound variables, using implicit substitution. (Contributed by BTernaryTau, 31-Jul-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑦𝜒))
Theorem	dvelimalcased 35472*	Eliminate a disjoint variable condition from a universally quantified statement using cases. (Contributed by BTernaryTau, 31-Jul-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜃)    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑥 → (𝜓 → 𝜃)))    &   ⊢ ((𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (𝜒 → 𝜃))    &   ⊢ (𝜑 → ∀𝑧𝜓)    &   ⊢ (𝜑 → ∀𝑥𝜒)    ⇒   ⊢ (𝜑 → ∀𝑥𝜃)
Theorem	dvelimalcasei 35473*	Eliminate a disjoint variable condition from a universally quantified statement using cases. Inference form of dvelimalcased 35472. See axsepg2 35561 for an example of its use. (Contributed by BTernaryTau, 31-Jul-2025.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜒)    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑥 → (𝜑 → 𝜒)))    &   ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜓 → 𝜒))    &   ⊢ ∀𝑧𝜑    &   ⊢ ∀𝑥𝜓    ⇒   ⊢ ∀𝑥𝜒
Theorem	dvelimexcased 35474*	Eliminate a disjoint variable condition from an existentially quantified statement using cases. (Contributed by BTernaryTau, 31-Jul-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜃)    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑥 → (𝜓 → 𝜃)))    &   ⊢ ((𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (𝜒 → 𝜃))    &   ⊢ (𝜑 → ∃𝑧𝜓)    &   ⊢ (𝜑 → ∃𝑥𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥𝜃)
Theorem	dvelimexcasei 35475*	Eliminate a disjoint variable condition from an existentially quantified statement using cases. Inference form of dvelimexcased 35474. See axnulg 35566 for an example of its use. (Contributed by BTernaryTau, 31-Jul-2025.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜒)    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑥 → (𝜑 → 𝜒)))    &   ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜓 → 𝜒))    &   ⊢ ∃𝑧𝜑    &   ⊢ ∃𝑥𝜓    ⇒   ⊢ ∃𝑥𝜒
21.5.2  ZF set theory
Theorem	inv2 35476	The intersection of the universal class with a class is itself. A commuted form of inv1 4354. (Contributed by BTernaryTau, 24-Jun-2026.)
⊢ (V ∩ 𝐴) = 𝐴
Theorem	exdifsn 35477	There exists an element in a class excluding a singleton if and only if there exists an element in the original class not equal to the singleton element. (Contributed by BTernaryTau, 15-Sep-2023.)
⊢ (∃𝑥 𝑥 ∈ (𝐴 ∖ {𝐵}) ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 𝐵)
Theorem	srcmpltd 35478	If a statement is true for every element of a class and for every element of its complement relative to a second class, then it is true for every element in the second class. (Contributed by BTernaryTau, 27-Sep-2023.)
⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝜓))    &   ⊢ (𝜑 → (𝐶 ∈ (𝐵 ∖ 𝐴) → 𝜓))    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐵 → 𝜓))
Theorem	prsrcmpltd 35479	If a statement is true for all pairs of elements of a class, all pairs of elements of its complement relative to a second class, and all pairs with one element in each, then it is true for all pairs of elements of the second class. (Contributed by BTernaryTau, 27-Sep-2023.)
⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → 𝜓))    &   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ (𝐵 ∖ 𝐴)) → 𝜓))    &   ⊢ (𝜑 → ((𝐶 ∈ (𝐵 ∖ 𝐴) ∧ 𝐷 ∈ 𝐴) → 𝜓))    &   ⊢ (𝜑 → ((𝐶 ∈ (𝐵 ∖ 𝐴) ∧ 𝐷 ∈ (𝐵 ∖ 𝐴)) → 𝜓))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → 𝜓))
Theorem	axnulALT2 35480*	Alternate proof of axnul 5267, proved from propositional calculus, ax-gen 1824, ax-4 1838, ax-6 1996, and ax-rep 5237. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by BTernaryTau, 27-Mar-2026.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	dff15 35481*	A one-to-one function in terms of different arguments never having the same function value. (Contributed by BTernaryTau, 24-Oct-2023.)
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)))
Theorem	f1resveqaeq 35482	If a function restricted to a class is one-to-one, then for any two elements of the class, the values of the function at those elements are equal only if the two elements are the same element. (Contributed by BTernaryTau, 27-Sep-2023.)
⊢ (((𝐹 ↾ 𝐴):𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷))
Theorem	f1resrcmplf1dlem 35483	Lemma for f1resrcmplf1d 35484. (Contributed by BTernaryTau, 27-Sep-2023.)
⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ((𝐹 “ 𝐶) ∩ (𝐹 “ 𝐷)) = ∅)    ⇒   ⊢ (𝜑 → ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐷) → ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑋 = 𝑌)))
Theorem	f1resrcmplf1d 35484	If a function's restriction to a subclass of its domain and its restriction to the relative complement of that subclass are both one-to-one, and if the ranges of those two restrictions are disjoint, then the function is itself one-to-one. (Contributed by BTernaryTau, 28-Sep-2023.)
⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶–1-1→𝐵)    &   ⊢ (𝜑 → (𝐹 ↾ (𝐴 ∖ 𝐶)):(𝐴 ∖ 𝐶)–1-1→𝐵)    &   ⊢ (𝜑 → ((𝐹 “ 𝐶) ∩ (𝐹 “ (𝐴 ∖ 𝐶))) = ∅)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵)
Theorem	fnfvintima 35485*	Condition for a function value to equal the intersection of an image that contains it. (Contributed by BTernaryTau, 23-Jun-2026.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹‘𝐶) = ∩ (𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝐶) ⊆ (𝐹‘𝑥)))
Theorem	funen1cnv 35486	If a function is equinumerous to ordinal 1, then its converse is also a function. (Contributed by BTernaryTau, 8-Oct-2023.)
⊢ ((Fun 𝐹 ∧ 𝐹 ≈ 1o) → Fun ◡𝐹)
Theorem	ordprcon 35487	If an ordinal class is not a set, then it must be the proper class of all ordinals. (Contributed by BTernaryTau, 9-Jun-2026.)
⊢ ((Ord 𝐴 ∧ ¬ 𝐴 ∈ V) → 𝐴 = On)
Theorem	xoromon 35488	ω is either an ordinal set or the proper class of all ordinal sets, but not both. This is a stronger version of omon 7872. (Contributed by BTernaryTau, 25-Jan-2026.)
⊢ (ω ∈ On ⊻ ω = On)
Theorem	fissorduni 35489	The union (supremum) of a finite set of ordinals less than a nonzero ordinal class is an element of that ordinal class. (Contributed by BTernaryTau, 15-Jan-2026.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (Ord 𝐵 ∧ 𝐵 ≠ ∅)) → ∪ 𝐴 ∈ 𝐵)
Theorem	ordtypeon 35490	A proper class with a set-like well-ordering is isomorphic to the proper class of all ordinal numbers. (Contributed by BTernaryTau, 9-Jun-2026.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ¬ 𝐴 ∈ V) → 𝐹 Isom E , 𝑅 (On, 𝐴))
Theorem	fnrelpredd 35491*	A function that preserves a relation also preserves predecessors. (Contributed by BTernaryTau, 16-Jul-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐹‘𝑥)𝑆(𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ (𝜑 → Pred(𝑆, (𝐹 “ 𝐶), (𝐹‘𝐷)) = (𝐹 “ Pred(𝑅, 𝐶, 𝐷)))
Theorem	cardpred 35492	The cardinality function preserves predecessors. (Contributed by BTernaryTau, 18-Jul-2024.)
⊢ ((𝐴 ⊆ dom card ∧ 𝐵 ∈ dom card) → Pred( E , (card “ 𝐴), (card‘𝐵)) = (card “ Pred( ≺ , 𝐴, 𝐵)))
Theorem	nummin 35493*	Every nonempty class of numerable sets has a minimal element. (Contributed by BTernaryTau, 18-Jul-2024.)
⊢ ((𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 Pred( ≺ , 𝐴, 𝑥) = ∅)
Theorem	1enumen 35494*	The Fundamental Theorem of Enumeration (see https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/enu.pdf), extended to all sets. The expression ∪ 𝑥 ∈ 𝐴({𝑥} × 𝐵) can be thought of as expressing an indexed disjoint union ⊔ 𝑥 ∈ 𝐴𝐵 where each 𝐵 has its elements tagged with the set 𝑥 that generated it. See the comment directly before undjudom 10158 for context on disjoint union as a representation of cardinal addition. This theorem is not limited to numerable sets, but it also does not depend on AC. See 1enumcard 35495 for a version that uses the card function, 1enumkard 35593 for a version that uses the kard function , and 1enum 35617 for a version that uses an explicit sum of complex number 1s. (Contributed by BTernaryTau, 26-Jun-2026.)
⊢ (𝐴 ∈ V → 𝐴 ≈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 1o))
Theorem	1enumcard 35495*	The Fundamental Theorem of Enumeration (see https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/enu.pdf), extended to all sets. The expression ∪ 𝑥 ∈ 𝐴({𝑥} × 𝐵) can be thought of as expressing an indexed disjoint union ⊔ 𝑥 ∈ 𝐴𝐵 where each 𝐵 has its elements tagged with the set 𝑥 that generated it. See the comment directly before undjudom 10158 for context on disjoint union as a representation of cardinal addition. This theorem does not depend on AC, but it is only meaningful for numerable sets. See 1enumen 35494 and 1enumkard 35593 for versions that are meaningful for non-numerable sets, and see 1enum 35617 for a version that uses an explicit sum of complex number 1s. (Contributed by BTernaryTau, 26-Jun-2026.)
⊢ (𝐴 ∈ V → (card‘𝐴) = (card‘∪ 𝑥 ∈ 𝐴 ({𝑥} × 1o)))
Theorem	r11 35496	Value of the cumulative hierarchy of sets function at 1o. (Contributed by BTernaryTau, 24-Jan-2026.)
⊢ (𝑅1‘1o) = 1o
Theorem	r12 35497	Value of the cumulative hierarchy of sets function at 2o. (Contributed by BTernaryTau, 25-Jan-2026.)
⊢ (𝑅1‘2o) = 2o
Theorem	r1wf 35498	Each stage in the cumulative hierarchy is well-founded. (Contributed by BTernaryTau, 19-Jan-2026.)
⊢ (𝑅1‘𝐴) ∈ ∪ (𝑅1 “ On)
Theorem	elwf 35499	An element of a well-founded set is well-founded. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ ∪ (𝑅1 “ On))
Theorem	r1elcl 35500	Each set of the cumulative hierarchy is closed under membership. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ (𝑅1‘𝐵))