Metamath Proof Explorer

Theorem bnj66

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 bnj66.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj66.2 ⊢ Y = x f ↾ pred x A R
bnj66.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
Assertion bnj66 ⊢ g ∈ C → Rel ⁡ g

Proof

Step Hyp Ref Expression
1 bnj66.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj66.2 ⊢ Y = x f ↾ pred x A R
3 bnj66.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 fneq1 ⊢ g = f → g Fn d ↔ f Fn d
5 fveq1 ⊢ g = f → g ⁡ x = f ⁡ x
6 reseq1 ⊢ g = f → g ↾ pred x A R = f ↾ pred x A R
7 6 opeq2d ⊢ g = f → x g ↾ pred x A R = x f ↾ pred x A R
8 7 2 eqtr4di ⊢ g = f → x g ↾ pred x A R = Y
9 8 fveq2d ⊢ g = f → G ⁡ x g ↾ pred x A R = G ⁡ Y
10 5 9 eqeq12d ⊢ g = f → g ⁡ x = G ⁡ x g ↾ pred x A R ↔ f ⁡ x = G ⁡ Y
11 10 ralbidv ⊢ g = f → ∀ x ∈ d g ⁡ x = G ⁡ x g ↾ pred x A R ↔ ∀ x ∈ d f ⁡ x = G ⁡ Y
12 4 11 anbi12d ⊢ g = f → g Fn d ∧ ∀ x ∈ d g ⁡ x = G ⁡ x g ↾ pred x A R ↔ f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
13 12 rexbidv ⊢ g = f → ∃ d ∈ B g Fn d ∧ ∀ x ∈ d g ⁡ x = G ⁡ x g ↾ pred x A R ↔ ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
14 13 cbvabv ⊢ g | ∃ d ∈ B g Fn d ∧ ∀ x ∈ d g ⁡ x = G ⁡ x g ↾ pred x A R = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
15 3 14 eqtr4i ⊢ C = g | ∃ d ∈ B g Fn d ∧ ∀ x ∈ d g ⁡ x = G ⁡ x g ↾ pred x A R
16 15 bnj1436 ⊢ g ∈ C → ∃ d ∈ B g Fn d ∧ ∀ x ∈ d g ⁡ x = G ⁡ x g ↾ pred x A R
17 bnj1239 ⊢ ∃ d ∈ B g Fn d ∧ ∀ x ∈ d g ⁡ x = G ⁡ x g ↾ pred x A R → ∃ d ∈ B g Fn d
18 fnrel ⊢ g Fn d → Rel ⁡ g
19 18 rexlimivw ⊢ ∃ d ∈ B g Fn d → Rel ⁡ g
20 16 17 19 3syl ⊢ g ∈ C → Rel ⁡ g