Metamath Proof Explorer

Theorem bnj1514

Description: Technical lemma for bnj1500 . 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 bnj1514.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj1514.2 ⊢ Y = x f ↾ pred x A R
bnj1514.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
Assertion bnj1514 ⊢ f ∈ C → ∀ x ∈ dom ⁡ f f ⁡ x = G ⁡ Y

Proof

Step Hyp Ref Expression
1 bnj1514.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1514.2 ⊢ Y = x f ↾ pred x A R
3 bnj1514.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 3 bnj1436 ⊢ f ∈ C → ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
5 df-rex ⊢ ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y ↔ ∃ d d ∈ B ∧ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
6 3anass ⊢ d ∈ B ∧ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y ↔ d ∈ B ∧ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
7 5 6 bnj133 ⊢ ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y ↔ ∃ d d ∈ B ∧ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
8 4 7 sylib ⊢ f ∈ C → ∃ d d ∈ B ∧ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
9 simp3 ⊢ d ∈ B ∧ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y → ∀ x ∈ d f ⁡ x = G ⁡ Y
10 fndm ⊢ f Fn d → dom ⁡ f = d
11 10 3ad2ant2 ⊢ d ∈ B ∧ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y → dom ⁡ f = d
12 11 raleqdv ⊢ d ∈ B ∧ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y → ∀ x ∈ dom ⁡ f f ⁡ x = G ⁡ Y ↔ ∀ x ∈ d f ⁡ x = G ⁡ Y
13 9 12 mpbird ⊢ d ∈ B ∧ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y → ∀ x ∈ dom ⁡ f f ⁡ x = G ⁡ Y
14 8 13 bnj593 ⊢ f ∈ C → ∃ d ∀ x ∈ dom ⁡ f f ⁡ x = G ⁡ Y
15 14 bnj937 ⊢ f ∈ C → ∀ x ∈ dom ⁡ f f ⁡ x = G ⁡ Y