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∈dpredxAR⊆d
bnj1514.2 ⊢Y=xf↾predxAR
bnj1514.3 ⊢C=f|∃d∈BfFnd∧∀x∈df⁡x=G⁡Y
Assertion bnj1514 ⊢f∈C→∀x∈dom⁡ff⁡x=G⁡Y

Proof

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