Metamath Proof Explorer

Theorem bnj1256

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 bnj1256.1 ⊢B=d|d⊆A∧∀x∈dpredxAR⊆d
bnj1256.2 ⊢Y=xf↾predxAR
bnj1256.3 ⊢C=f|∃d∈BfFnd∧∀x∈df⁡x=G⁡Y
bnj1256.4 ⊢D=dom⁡g∩dom⁡h
bnj1256.5 ⊢E=x∈D|g⁡x≠h⁡x
bnj1256.6 ⊢φ↔RFrSeA∧g∈C∧h∈C∧g↾D≠h↾D
bnj1256.7 ⊢ψ↔φ∧x∈E∧∀y∈E¬yRx
Assertion bnj1256 ⊢φ→∃d∈BgFnd

Proof

Step Hyp Ref Expression
1 bnj1256.1 ⊢B=d|d⊆A∧∀x∈dpredxAR⊆d
2 bnj1256.2 ⊢Y=xf↾predxAR
3 bnj1256.3 ⊢C=f|∃d∈BfFnd∧∀x∈df⁡x=G⁡Y
4 bnj1256.4 ⊢D=dom⁡g∩dom⁡h
5 bnj1256.5 ⊢E=x∈D|g⁡x≠h⁡x
6 bnj1256.6 ⊢φ↔RFrSeA∧g∈C∧h∈C∧g↾D≠h↾D
7 bnj1256.7 ⊢ψ↔φ∧x∈E∧∀y∈E¬yRx
8 abid ⊢g∈g|∃d∈BgFnd∧∀x∈dg⁡x=G⁡xg↾predxAR↔∃d∈BgFnd∧∀x∈dg⁡x=G⁡xg↾predxAR
9 8 bnj1238 ⊢g∈g|∃d∈BgFnd∧∀x∈dg⁡x=G⁡xg↾predxAR→∃d∈BgFnd
10 eqid ⊢xg↾predxAR=xg↾predxAR
11 eqid ⊢g|∃d∈BgFnd∧∀x∈dg⁡x=G⁡xg↾predxAR=g|∃d∈BgFnd∧∀x∈dg⁡x=G⁡xg↾predxAR
12 2 3 10 11 bnj1234 ⊢C=g|∃d∈BgFnd∧∀x∈dg⁡x=G⁡xg↾predxAR
13 9 12 eleq2s ⊢g∈C→∃d∈BgFnd
14 6 13 bnj770 ⊢φ→∃d∈BgFnd