P. 347 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34601-34700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bnj1398 34601*	Technical lemma for bnj60 34629. 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 34602*	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)
Theorem	bnj1408 34603*	Technical lemma for bnj1414 34604. 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 34604*	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)
Theorem	bnj1415 34605*	Technical lemma for bnj60 34629. 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 34606	Technical lemma for bnj60 34629. 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 34607	Property of pred. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → 𝑦𝑅𝑥)
Theorem	bnj1417 34608*	Technical lemma for bnj60 34629. 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 34609*	Technical lemma for bnj60 34629. 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 34610*	Technical lemma for bnj60 34629. 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 34611*	Technical lemma for bnj60 34629. 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 34612*	Technical lemma for bnj60 34629. 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 34613*	Technical lemma for bnj60 34629. 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 34614*	Technical lemma for bnj60 34629. 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 34615*	Technical lemma for bnj60 34629. 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 34616*	Technical lemma for bnj60 34629. 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 34617*	Technical lemma for bnj60 34629. 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 34618*	Technical lemma for bnj60 34629. 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 34619*	Technical lemma for bnj60 34629. 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 34620*	Technical lemma for bnj60 34629. 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 34621*	Technical lemma for bnj60 34629. 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 34622*	Technical lemma for bnj60 34629. 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 34623*	Technical lemma for bnj60 34629. 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 34624*	Technical lemma for bnj60 34629. 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 34625*	Technical lemma for bnj60 34629. 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 34626*	Technical lemma for bnj60 34629. 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 34627*	Technical lemma for bnj60 34629. 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 34628*	Technical lemma for bnj60 34629. 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 34629*	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 34630*	Technical lemma for bnj1500 34635. 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 34631*	Technical lemma for bnj1500 34635. 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 34632*	Technical lemma for bnj1500 34635. 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 34633*	Technical lemma for bnj1500 34635. 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 34634*	Technical lemma for bnj1500 34635. 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 34635*	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 34636*	Technical lemma for bnj1522 34639. 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 34637*	Technical lemma for bnj1522 34639. 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 34638*	Technical lemma for bnj1522 34639. 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 34639*	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  ZF set theory
Theorem	exdifsn 34640	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 34641	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 34642	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	dff15 34643*	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 34644	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 34645	Lemma for f1resrcmplf1d 34646. (Contributed by BTernaryTau, 27-Sep-2023.)
⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ((𝐹 “ 𝐶) ∩ (𝐹 “ 𝐷)) = ∅)    ⇒   ⊢ (𝜑 → ((𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐷) → ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑋 = 𝑌)))
Theorem	f1resrcmplf1d 34646	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	funen1cnv 34647	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	fnrelpredd 34648*	A function that preserves a relation also preserves predecessors. (Contributed by BTernaryTau, 16-Jul-2024.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐹‘𝑥)𝑆(𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ (𝜑 → Pred(𝑆, (𝐹 “ 𝐶), (𝐹‘𝐷)) = (𝐹 “ Pred(𝑅, 𝐶, 𝐷)))
Theorem	cardpred 34649	The cardinality function preserves predecessors. (Contributed by BTernaryTau, 18-Jul-2024.)
⊢ ((𝐴 ⊆ dom card ∧ 𝐵 ∈ dom card) → Pred( E , (card “ 𝐴), (card‘𝐵)) = (card “ Pred( ≺ , 𝐴, 𝐵)))
Theorem	nummin 34650*	Every nonempty class of numerable sets has a minimal element. (Contributed by BTernaryTau, 18-Jul-2024.)
⊢ ((𝐴 ⊆ dom card ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 Pred( ≺ , 𝐴, 𝑥) = ∅)
21.5.1.1  Finitism
Theorem	fineqvrep 34651*	If the Axiom of Infinity is negated, then the Axiom of Replacement becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.)
⊢ (Fin = V → (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))
Theorem	fineqvpow 34652*	If the Axiom of Infinity is negated, then the Axiom of Power Sets becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.)
⊢ (Fin = V → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
Theorem	fineqvac 34653	If the Axiom of Infinity is negated, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep 5279 and ax-pow 5359, see fineqvacALT 34654. (Contributed by BTernaryTau, 21-Sep-2024.)
⊢ (Fin = V → CHOICE)
Theorem	fineqvacALT 34654	Shorter proof of fineqvac 34653 using ax-rep 5279 and ax-pow 5359. (Contributed by BTernaryTau, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fin = V → CHOICE)
21.5.2  Real and complex numbers
Theorem	zltp1ne 34655	Integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	nnltp1ne 34656	Positive integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	nn0ltp1ne 34657	Nonnegative integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	0nn0m1nnn0 34658	A number is zero if and only if it's a nonnegative integer that becomes negative after subtracting 1. (Contributed by BTernaryTau, 30-Sep-2023.)
⊢ (𝑁 = 0 ↔ (𝑁 ∈ ℕ0 ∧ ¬ (𝑁 − 1) ∈ ℕ0))
Theorem	f1resfz0f1d 34659	If a function with a sequence of nonnegative integers (starting at 0) as its domain is one-to-one when 0 is removed, and if the range of that restriction does not contain the function's value at the removed integer, then the function is itself one-to-one. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹:(0...𝐾)⟶𝑉)    &   ⊢ (𝜑 → (𝐹 ↾ (1...𝐾)):(1...𝐾)–1-1→𝑉)    &   ⊢ (𝜑 → ((𝐹 “ {0}) ∩ (𝐹 “ (1...𝐾))) = ∅)    ⇒   ⊢ (𝜑 → 𝐹:(0...𝐾)–1-1→𝑉)
Theorem	fisshasheq 34660	A finite set is equal to its subset if they are the same size. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝐴 = 𝐵)
Theorem	revpfxsfxrev 34661	The reverse of a prefix of a word is equal to the same-length suffix of the reverse of that word. (Contributed by BTernaryTau, 2-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) = ((reverse‘𝑊) substr ⟨((♯‘𝑊) − 𝐿), (♯‘𝑊)⟩))
Theorem	swrdrevpfx 34662	A subword expressed in terms of reverses and prefixes. (Contributed by BTernaryTau, 3-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑊 substr ⟨𝐹, 𝐿⟩) = (reverse‘((reverse‘(𝑊 prefix 𝐿)) prefix (𝐿 − 𝐹))))
21.5.3  Graph theory
Theorem	lfuhgr 34663*	A hypergraph is loop-free if and only if every edge connects at least two vertices. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)2 ≤ (♯‘𝑥)))
Theorem	lfuhgr2 34664*	A hypergraph is loop-free if and only if every edge is not a loop. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)(♯‘𝑥) ≠ 1))
Theorem	lfuhgr3 34665*	A hypergraph is loop-free if and only if none of its edges connect to only one vertex. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ¬ ∃𝑎{𝑎} ∈ (Edg‘𝐺)))
Theorem	cplgredgex 34666*	Any two (distinct) vertices in a complete graph are connected to each other by at least one edge. (Contributed by BTernaryTau, 2-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒))
Theorem	cusgredgex 34667	Any two (distinct) vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → {𝐴, 𝐵} ∈ 𝐸))
Theorem	cusgredgex2 34668	Any two distinct vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝐸))
Theorem	pfxwlk 34669	A prefix of a walk is a walk. (Contributed by BTernaryTau, 2-Dec-2023.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝐿)(Walks‘𝐺)(𝑃 prefix (𝐿 + 1)))
Theorem	revwlk 34670	The reverse of a walk is a walk. (Contributed by BTernaryTau, 30-Nov-2023.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃))
Theorem	revwlkb 34671	Two words represent a walk if and only if their reverses also represent a walk. (Contributed by BTernaryTau, 4-Dec-2023.)
⊢ ((𝐹 ∈ Word 𝑊 ∧ 𝑃 ∈ Word 𝑈) → (𝐹(Walks‘𝐺)𝑃 ↔ (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃)))
Theorem	swrdwlk 34672	Two matching subwords of a walk also represent a walk. (Contributed by BTernaryTau, 7-Dec-2023.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐵 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 substr ⟨𝐵, 𝐿⟩)(Walks‘𝐺)(𝑃 substr ⟨𝐵, (𝐿 + 1)⟩))
Theorem	pthhashvtx 34673	A graph containing a path has at least as many vertices as there are edges in the path. (Contributed by BTernaryTau, 5-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘𝐹) ≤ (♯‘𝑉))
Theorem	pthisspthorcycl 34674	A path is either a simple path or a cycle (or both). (Contributed by BTernaryTau, 20-Oct-2023.)
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝐹(SPaths‘𝐺)𝑃 ∨ 𝐹(Cycles‘𝐺)𝑃))
Theorem	spthcycl 34675	A walk is a trivial path if and only if it is both a simple path and a cycle. (Contributed by BTernaryTau, 8-Oct-2023.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 𝐹 = ∅) ↔ (𝐹(SPaths‘𝐺)𝑃 ∧ 𝐹(Cycles‘𝐺)𝑃))
Theorem	usgrgt2cycl 34676	A non-trivial cycle in a simple graph has a length greater than 2. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝐹))
Theorem	usgrcyclgt2v 34677	A simple graph with a non-trivial cycle must have at least 3 vertices. (Contributed by BTernaryTau, 5-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝑉))
Theorem	subgrwlk 34678	If a walk exists in a subgraph of a graph 𝐺, then that walk also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Walks‘𝑆)𝑃 → 𝐹(Walks‘𝐺)𝑃))
Theorem	subgrtrl 34679	If a trail exists in a subgraph of a graph 𝐺, then that trail also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Trails‘𝑆)𝑃 → 𝐹(Trails‘𝐺)𝑃))
Theorem	subgrpth 34680	If a path exists in a subgraph of a graph 𝐺, then that path also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Paths‘𝑆)𝑃 → 𝐹(Paths‘𝐺)𝑃))
Theorem	subgrcycl 34681	If a cycle exists in a subgraph of a graph 𝐺, then that cycle also exists in 𝐺. (Contributed by BTernaryTau, 23-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Cycles‘𝑆)𝑃 → 𝐹(Cycles‘𝐺)𝑃))
Theorem	cusgr3cyclex 34682*	Every complete simple graph with more than two vertices has a 3-cycle. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 2 < (♯‘𝑉)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))
Theorem	loop1cycl 34683*	A hypergraph has a cycle of length one if and only if it has a loop. (Contributed by BTernaryTau, 13-Oct-2023.)
⊢ (𝐺 ∈ UHGraph → (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ {𝐴} ∈ (Edg‘𝐺)))
Theorem	2cycld 34684	Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)
Theorem	2cycl2d 34685	Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐴”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐴, 𝐵} ⊆ (𝐼‘𝐾)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    ⇒   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)
Theorem	umgr2cycllem 34686*	Lemma for umgr2cycl 34687. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    &   ⊢ (𝜑 → 𝐽 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → (𝐼‘𝐽) = (𝐼‘𝐾))    ⇒   ⊢ (𝜑 → ∃𝑝 𝐹(Cycles‘𝐺)𝑝)
Theorem	umgr2cycl 34687*	A multigraph with two distinct edges that connect the same vertices has a 2-cycle. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ ∃𝑗 ∈ dom 𝐼∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2))
21.5.3.1  Acyclic graphs
Syntax	cacycgr 34688	Extend class notation with acyclic graphs.
class AcyclicGraph
Definition	df-acycgr 34689*	Define the class of all acyclic graphs. A graph is called acyclic if it has no (non-trivial) cycles. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}
Theorem	dfacycgr1 34690*	An alternate definition of the class of all acyclic graphs that requires all cycles to be trivial. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ AcyclicGraph = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}
Theorem	isacycgr 34691*	The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅)))
Theorem	isacycgr1 34692*	The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝐺)𝑝 → 𝑓 = ∅)))
Theorem	acycgrcycl 34693	Any cycle in an acyclic graph is trivial (i.e. has one vertex and no edges). (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → 𝐹 = ∅)
Theorem	acycgr0v 34694	A null graph (with no vertices) is an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑉 = ∅) → 𝐺 ∈ AcyclicGraph)
Theorem	acycgr1v 34695	A multigraph with one vertex is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ (♯‘𝑉) = 1) → 𝐺 ∈ AcyclicGraph)
Theorem	acycgr2v 34696	A simple graph with two vertices is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝑉) = 2) → 𝐺 ∈ AcyclicGraph)
Theorem	prclisacycgr 34697*	A proper class (representing a null graph, see vtxvalprc 28845) has the property of an acyclic graph (see also acycgr0v 34694). (Contributed by BTernaryTau, 11-Oct-2023.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (¬ 𝐺 ∈ V → ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅))
Theorem	acycgrislfgr 34698*	An acyclic hypergraph is a loop-free hypergraph. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph) → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})
Theorem	upgracycumgr 34699	An acyclic pseudograph is a multigraph. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ UMGraph)
Theorem	umgracycusgr 34700	An acyclic multigraph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ USGraph)