Metamath Proof Explorer


Theorem bnj1259

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1259.1 𝐵 = { 𝑑 ∣ ( 𝑑𝐴 ∧ ∀ 𝑥𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1259.2 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1259.3 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
bnj1259.4 𝐷 = ( dom 𝑔 ∩ dom )
bnj1259.5 𝐸 = { 𝑥𝐷 ∣ ( 𝑔𝑥 ) ≠ ( 𝑥 ) }
bnj1259.6 ( 𝜑 ↔ ( 𝑅 FrSe 𝐴𝑔𝐶𝐶 ∧ ( 𝑔𝐷 ) ≠ ( 𝐷 ) ) )
bnj1259.7 ( 𝜓 ↔ ( 𝜑𝑥𝐸 ∧ ∀ 𝑦𝐸 ¬ 𝑦 𝑅 𝑥 ) )
Assertion bnj1259 ( 𝜑 → ∃ 𝑑𝐵 Fn 𝑑 )

Proof

Step Hyp Ref Expression
1 bnj1259.1 𝐵 = { 𝑑 ∣ ( 𝑑𝐴 ∧ ∀ 𝑥𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1259.2 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1259.3 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
4 bnj1259.4 𝐷 = ( dom 𝑔 ∩ dom )
5 bnj1259.5 𝐸 = { 𝑥𝐷 ∣ ( 𝑔𝑥 ) ≠ ( 𝑥 ) }
6 bnj1259.6 ( 𝜑 ↔ ( 𝑅 FrSe 𝐴𝑔𝐶𝐶 ∧ ( 𝑔𝐷 ) ≠ ( 𝐷 ) ) )
7 bnj1259.7 ( 𝜓 ↔ ( 𝜑𝑥𝐸 ∧ ∀ 𝑦𝐸 ¬ 𝑦 𝑅 𝑥 ) )
8 abid ( ∈ { ∣ ∃ 𝑑𝐵 ( Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } ↔ ∃ 𝑑𝐵 ( Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
9 8 bnj1238 ( ∈ { ∣ ∃ 𝑑𝐵 ( Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } → ∃ 𝑑𝐵 Fn 𝑑 )
10 eqid 𝑥 , ( ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑥 , ( ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
11 eqid { ∣ ∃ 𝑑𝐵 ( Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) } = { ∣ ∃ 𝑑𝐵 ( Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) }
12 2 3 10 11 bnj1234 𝐶 = { ∣ ∃ 𝑑𝐵 ( Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) }
13 9 12 eleq2s ( 𝐶 → ∃ 𝑑𝐵 Fn 𝑑 )
14 6 13 bnj771 ( 𝜑 → ∃ 𝑑𝐵 Fn 𝑑 )