P. 356 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35501-35600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bnj1345 35501	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥(𝜓 ∧ 𝜒))    &   ⊢ (𝜃 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))    &   ⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (𝜑 → ∃𝑥𝜃)
Theorem	bnj1350 35502*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	bnj1351 35503*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
Theorem	bnj1352 35504*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
Theorem	bnj1361 35505*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	bnj1366 35506*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ (𝜓 ↔ (𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑 ∧ 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝜑}))    ⇒   ⊢ (𝜓 → 𝐵 ∈ V)
Theorem	bnj1379 35507*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)    &   ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)    &   ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))    &   ⊢ (𝜒 ↔ (𝜓 ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ ∪ 𝐴))    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑓 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑓))    &   ⊢ (𝜏 ↔ (𝜃 ∧ 𝑔 ∈ 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝑔))    ⇒   ⊢ (𝜓 → Fun ∪ 𝐴)
Theorem	bnj1383 35508*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)    &   ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)    &   ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))    ⇒   ⊢ (𝜓 → Fun ∪ 𝐴)
Theorem	bnj1385 35509*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)    &   ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)    &   ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))    &   ⊢ (𝑥 ∈ 𝐴 → ∀𝑓 𝑥 ∈ 𝐴)    &   ⊢ (𝜑′ ↔ ∀ℎ ∈ 𝐴 Fun ℎ)    &   ⊢ 𝐸 = (dom ℎ ∩ dom 𝑔)    &   ⊢ (𝜓′ ↔ (𝜑′ ∧ ∀ℎ ∈ 𝐴 ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸)))    ⇒   ⊢ (𝜓 → Fun ∪ 𝐴)
Theorem	bnj1386 35510*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓)    &   ⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔)    &   ⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)))    &   ⊢ (𝑥 ∈ 𝐴 → ∀𝑓 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜓 → Fun ∪ 𝐴)
Theorem	bnj1397 35511	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bnj1400 35512*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥
Theorem	bnj1405 35513*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝑋 ∈ ∪ 𝑦 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ∈ 𝐵)
Theorem	bnj1422 35514	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → Fun 𝐴)    &   ⊢ (𝜑 → dom 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 Fn 𝐵)
Theorem	bnj1424 35515	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = (𝐵 ∪ 𝐶)    ⇒   ⊢ (𝐷 ∈ 𝐴 → (𝐷 ∈ 𝐵 ∨ 𝐷 ∈ 𝐶))
Theorem	bnj1436 35516	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝑥 ∈ 𝐴 → 𝜑)
Theorem	bnj1441 35517*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Add disjoint variable condition to avoid ax-13 2401. See bnj1441g 35518 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → ∀𝑦 𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	bnj1441g 35518*	First-order logic and set theory. See bnj1441 35517 for a version with more disjoint variable conditions, but not requiring ax-13 2401. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → ∀𝑦 𝑧 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
Theorem	bnj1454 35519	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝐵 ∈ V → (𝐵 ∈ 𝐴 ↔ [𝐵 / 𝑥]𝜑))
Theorem	bnj1459 35520*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐴))    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜒)
Theorem	bnj1464 35521*	Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
Theorem	bnj1465 35522*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑉) → ∃𝑥𝜑)
Theorem	bnj1468 35523*	Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
Theorem	bnj1476 35524	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}    &   ⊢ (𝜓 → 𝐷 = ∅)    ⇒   ⊢ (𝜓 → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	bnj1502 35525	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))
Theorem	bnj1503 35526	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐹)    &   ⊢ (𝜑 → 𝐴 ⊆ dom 𝐺)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴))
Theorem	bnj1517 35527	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = {𝑥 ∣ (𝜑 ∧ 𝜓)}    ⇒   ⊢ (𝑥 ∈ 𝐴 → 𝜓)
Theorem	bnj1521 35528	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 → ∃𝑥 ∈ 𝐵 𝜑)    &   ⊢ (𝜃 ↔ (𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜑))    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (𝜒 → ∃𝑥𝜃)
Theorem	bnj1533 35529	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 → ∀𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝐷)    &   ⊢ 𝐵 ⊆ 𝐴    &   ⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ 𝐶 ≠ 𝐸}    ⇒   ⊢ (𝜃 → ∀𝑧 ∈ 𝐵 𝐶 = 𝐸)
Theorem	bnj1534 35530*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐻‘𝑥)}    &   ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹)    ⇒   ⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ (𝐹‘𝑧) ≠ (𝐻‘𝑧)}
Theorem	bnj1536 35531*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵))
Theorem	bnj1538 35532	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}    ⇒   ⊢ (𝑥 ∈ 𝐴 → 𝜑)
Theorem	bnj1541 35533	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝐴 ≠ 𝐵))    &   ⊢ ¬ 𝜑    ⇒   ⊢ (𝜓 → 𝐴 = 𝐵)
Theorem	bnj1542 35534*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐺 Fn 𝐴)    &   ⊢ (𝜑 → 𝐹 ≠ 𝐺)    &   ⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) ≠ (𝐺‘𝑥))
21.5.2  Well founded induction and recursion
Theorem	bnj110 35535*	Well-founded induction restricted to a set (𝐴 ∈ V). The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	bnj157 35536*	Well-founded induction restricted to a set (𝐴 ∈ V). The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝑅 Fr 𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	bnj66 35537*	Technical lemma for bnj60 35739. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)}    &   ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩    &   ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}    ⇒   ⊢ (𝑔 ∈ 𝐶 → Rel 𝑔)
Theorem	bnj91 35538*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ ([𝑍 / 𝑦]𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj92 35539*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝑍 ∈ V    ⇒   ⊢ ([𝑍 / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑍 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj93 35540*	Technical lemma for bnj97 35543. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → pred(𝑥, 𝐴, 𝑅) ∈ V)
Theorem	bnj95 35541	Technical lemma for bnj124 35548. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ 𝐹 ∈ V
Theorem	bnj96 35542*	Technical lemma for bnj150 35553. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → dom 𝐹 = 1o)
Theorem	bnj97 35543*	Technical lemma for bnj150 35553. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj98 35544	Technical lemma for bnj150 35553. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))
Theorem	bnj106 35545*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐹 ∈ V    ⇒   ⊢ ([𝐹 / 𝑓][1o / 𝑛]𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj118 35546*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    ⇒   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj121 35547*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁)    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓)    ⇒   ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))
Theorem	bnj124 35548*	Technical lemma for bnj150 35553. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′)    &   ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))    ⇒   ⊢ (𝜁″ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 Fn 1o ∧ 𝜑″ ∧ 𝜓″)))
Theorem	bnj125 35549*	Technical lemma for bnj150 35553. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ (𝜑″ ↔ (𝐹‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj126 35550*	Technical lemma for bnj150 35553. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    ⇒   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj130 35551*	Technical lemma for bnj151 35554. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓)    &   ⊢ (𝜃′ ↔ [1o / 𝑛]𝜃)    ⇒   ⊢ (𝜃′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))
Theorem	bnj149 35552*	Technical lemma for bnj151 35554. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ (𝜃1 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜁0 ↔ (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0)    &   ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′)    &   ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′)    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    ⇒   ⊢ 𝜃1
Theorem	bnj150 35553*	Technical lemma for bnj151 35554. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓)    &   ⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′)    ⇒   ⊢ 𝜃0
Theorem	bnj151 35554*	Technical lemma for bnj153 35557. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜏 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜃))    &   ⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜑′ ↔ [1o / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [1o / 𝑛]𝜓)    &   ⊢ (𝜃′ ↔ [1o / 𝑛]𝜃)    &   ⊢ (𝜃0 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜃1 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜁′ ↔ [1o / 𝑛]𝜁)    &   ⊢ 𝐹 = {⟨∅, pred(𝑥, 𝐴, 𝑅)⟩}    &   ⊢ (𝜑″ ↔ [𝐹 / 𝑓]𝜑′)    &   ⊢ (𝜓″ ↔ [𝐹 / 𝑓]𝜓′)    &   ⊢ (𝜁″ ↔ [𝐹 / 𝑓]𝜁′)    &   ⊢ (𝜁0 ↔ (𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜁1 ↔ [𝑔 / 𝑓]𝜁0)    &   ⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′)    &   ⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′)    ⇒   ⊢ (𝑛 = 1o → ((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃))
Theorem	bnj154 35555*	Technical lemma for bnj153 35557. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑1 ↔ [𝑔 / 𝑓]𝜑′)    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    ⇒   ⊢ (𝜑1 ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
Theorem	bnj155 35556*	Technical lemma for bnj153 35557. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓1 ↔ [𝑔 / 𝑓]𝜓′)    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ (𝜓1 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 1o → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj153 35557*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜏 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜃))    ⇒   ⊢ (𝑛 = 1o → ((𝑛 ∈ 𝐷 ∧ 𝜏) → 𝜃))
Theorem	bnj207 35558*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑀 / 𝑛]𝜒)    &   ⊢ 𝑀 ∈ V    ⇒   ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑀 ∧ 𝜑′ ∧ 𝜓′)))
Theorem	bnj213 35559	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
Theorem	bnj222 35560*	Technical lemma for bnj229 35561. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ (𝜓 ↔ ∀𝑚 ∈ ω (suc 𝑚 ∈ 𝑁 → (𝐹‘suc 𝑚) = ∪ 𝑦 ∈ (𝐹‘𝑚) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj229 35561*	Technical lemma for bnj517 35562. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑛 ∈ 𝑁 ∧ (suc 𝑚 = 𝑛 ∧ 𝑚 ∈ ω ∧ 𝜓)) → (𝐹‘𝑛) ⊆ 𝐴)
Theorem	bnj517 35562*	Technical lemma for bnj518 35563. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) → ∀𝑛 ∈ 𝑁 (𝐹‘𝑛) ⊆ 𝐴)
Theorem	bnj518 35563*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜏 ↔ (𝜑 ∧ 𝜓 ∧ 𝑛 ∈ ω ∧ 𝑝 ∈ 𝑛))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏) → ∀𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V)
Theorem	bnj523 35564*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜑′ ↔ [𝑀 / 𝑛]𝜑)    &   ⊢ 𝑀 ∈ V    ⇒   ⊢ (𝜑′ ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅))
Theorem	bnj526 35565*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑋, 𝐴, 𝑅))
Theorem	bnj528 35566	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    ⇒   ⊢ 𝐺 ∈ V
Theorem	bnj535 35567*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝜑′ ∧ 𝜓′ ∧ 𝑚 ∈ ω ∧ 𝑝 ∈ 𝑚))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝑛 = (𝑚 ∪ {𝑚}) ∧ 𝑓 Fn 𝑚) → 𝐺 Fn 𝑛)
Theorem	bnj539 35568*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓′ ↔ [𝑀 / 𝑛]𝜓)    &   ⊢ 𝑀 ∈ V    ⇒   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑀 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj540 35569*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj543 35570*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)
Theorem	bnj544 35571*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)
Theorem	bnj545 35572	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    &   ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝜑″)
Theorem	bnj546 35573*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) ∈ V)
Theorem	bnj548 35574*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) ∧ 𝑖 ∈ 𝑚) → 𝐵 = 𝐾)
Theorem	bnj553 35575*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    ⇒   ⊢ (((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) ∧ 𝑖 ∈ 𝑚 ∧ 𝑝 = 𝑖) → (𝐺‘𝑚) = 𝐿)
Theorem	bnj554 35576*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    ⇒   ⊢ ((𝜂 ∧ 𝜁) → ((𝐺‘𝑚) = 𝐿 ↔ (𝐺‘suc 𝑖) = 𝐾))
Theorem	bnj556 35577	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    ⇒   ⊢ (𝜂 → 𝜎)
Theorem	bnj557 35578*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁) → (𝐺‘𝑚) = 𝐿)
Theorem	bnj558 35579*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜁) → (𝐺‘suc 𝑖) = 𝐾)
Theorem	bnj561 35580	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛)
Theorem	bnj562 35581	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝜑″)    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″)
Theorem	bnj570 35582*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖))    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛)    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂 ∧ 𝜌) → (𝐺‘suc 𝑖) = 𝐾)
Theorem	bnj571 35583*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    &   ⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛)    &   ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖))    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛)    &   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″)
Theorem	bnj605 35584*	Technical lemma. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))    &   ⊢ (𝜑″ ↔ [𝑓 / 𝑓]𝜑)    &   ⊢ (𝜓″ ↔ [𝑓 / 𝑓]𝜓)    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ 𝑓 ∈ V    &   ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜑″ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚∃𝑝𝜂)    &   ⊢ ((𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛) → 𝜒′)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝑓 Fn 𝑛)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″)    ⇒   ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
Theorem	bnj581 35585*	Technical lemma for bnj580 35590. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) Remove unnecessary distinct variable conditions. (Revised by Andrew Salmon, 9-Jul-2011.) (New usage is discouraged.)
⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)    &   ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)    &   ⊢ (𝜒′ ↔ [𝑔 / 𝑓]𝜒)    ⇒   ⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
Theorem	bnj589 35586*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑓‘suc 𝑘) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj590 35587	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    ⇒   ⊢ ((𝐵 = suc 𝑖 ∧ 𝜓) → (𝑖 ∈ ω → (𝐵 ∈ 𝑛 → (𝑓‘𝐵) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))))
Theorem	bnj591 35588*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))    ⇒   ⊢ ([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)))
Theorem	bnj594 35589*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))    &   ⊢ ([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)))    &   ⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))    ⇒   ⊢ ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)
Theorem	bnj580 35590*	Technical lemma for bnj579 35591. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    &   ⊢ (𝜑′ ↔ [𝑔 / 𝑓]𝜑)    &   ⊢ (𝜓′ ↔ [𝑔 / 𝑓]𝜓)    &   ⊢ (𝜒′ ↔ [𝑔 / 𝑓]𝜒)    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))    &   ⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))    ⇒   ⊢ (𝑛 ∈ 𝐷 → ∃*𝑓𝜒)
Theorem	bnj579 35591*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ (𝑛 ∈ 𝐷 → ∃*𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
Theorem	bnj602 35592	Equality theorem for the pred function constant. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝑋 = 𝑌 → pred(𝑋, 𝐴, 𝑅) = pred(𝑌, 𝐴, 𝑅))
Theorem	bnj607 35593*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ 𝐺 ∈ V    &   ⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)))    &   ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚∃𝑝𝜂)    &   ⊢ ((𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛) → 𝜒′)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″)    &   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″)    &   ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜑0 ↔ [ℎ / 𝑓]𝜑)    &   ⊢ (𝜓0 ↔ [ℎ / 𝑓]𝜓)    &   ⊢ (𝜑1 ↔ [𝐺 / ℎ]𝜑0)    &   ⊢ (𝜓1 ↔ [𝐺 / ℎ]𝜓0)    ⇒   ⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
Theorem	bnj609 35594*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑋, 𝐴, 𝑅))
Theorem	bnj611 35595*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)))
Theorem	bnj600 35596*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))    &   ⊢ (𝜑′ ↔ [𝑚 / 𝑛]𝜑)    &   ⊢ (𝜓′ ↔ [𝑚 / 𝑛]𝜓)    &   ⊢ (𝜒′ ↔ [𝑚 / 𝑛]𝜒)    &   ⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑)    &   ⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓)    &   ⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})    &   ⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))    &   ⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))    &   ⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))    &   ⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))    &   ⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖))    &   ⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅)    &   ⊢ 𝐺 = (𝑓 ∪ {⟨𝑚, 𝐶⟩})    ⇒   ⊢ (𝑛 ≠ 1o → ((𝑛 ∈ 𝐷 ∧ 𝜃) → 𝜒))
Theorem	bnj601 35597*	Technical lemma for bnj852 35598. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))    &   ⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))    ⇒   ⊢ (𝑛 ≠ 1o → ((𝑛 ∈ 𝐷 ∧ 𝜃) → 𝜒))
Theorem	bnj852 35598*	Technical lemma for bnj69 35687. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    ⇒   ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛 ∈ 𝐷 ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
Theorem	bnj864 35599*	Technical lemma for bnj69 35687. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷))    &   ⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    ⇒   ⊢ (𝜒 → ∃!𝑓𝜃)
Theorem	bnj865 35600*	Technical lemma for bnj69 35687. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))    &   ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))    &   ⊢ 𝐷 = (ω ∖ {∅})    &   ⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷))    &   ⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))    ⇒   ⊢ ∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃)