Metamath Proof Explorer

Theorem bnj1497

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

Proof

Step Hyp Ref Expression
1 bnj1497.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1497.2 ⊢ Y = x f ↾ pred x A R
3 bnj1497.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 3 bnj1317 ⊢ g ∈ C → ∀ f g ∈ C
5 4 nf5i ⊢ Ⅎ f g ∈ C
6 nfv ⊢ Ⅎ f Fun ⁡ g
7 5 6 nfim ⊢ Ⅎ f g ∈ C → Fun ⁡ g
8 eleq1w ⊢ f = g → f ∈ C ↔ g ∈ C
9 funeq ⊢ f = g → Fun ⁡ f ↔ Fun ⁡ g
10 8 9 imbi12d ⊢ f = g → f ∈ C → Fun ⁡ f ↔ g ∈ C → Fun ⁡ g
11 3 bnj1436 ⊢ f ∈ C → ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
12 11 bnj1299 ⊢ f ∈ C → ∃ d ∈ B f Fn d
13 fnfun ⊢ f Fn d → Fun ⁡ f
14 12 13 bnj31 ⊢ f ∈ C → ∃ d ∈ B Fun ⁡ f
15 14 bnj1265 ⊢ f ∈ C → Fun ⁡ f
16 7 10 15 chvarfv ⊢ g ∈ C → Fun ⁡ g
17 16 rgen ⊢ ∀ g ∈ C Fun ⁡ g