This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1307

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 bnj1307.1 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
bnj1307.2 ⊢ w ∈ B → ∀ x w ∈ B
Assertion bnj1307 ⊢ w ∈ C → ∀ x w ∈ C

Proof

Step Hyp Ref Expression
1 bnj1307.1 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
2 bnj1307.2 ⊢ w ∈ B → ∀ x w ∈ B
3 2 nfcii ⊢ Ⅎ _ x B
4 nfv ⊢ Ⅎ x f Fn d
5 nfra1 ⊢ Ⅎ x ∀ x ∈ d f ⁡ x = G ⁡ Y
6 4 5 nfan ⊢ Ⅎ x f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
7 3 6 nfrexw ⊢ Ⅎ x ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
8 7 nfab ⊢ Ⅎ _ x f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
9 1 8 nfcxfr ⊢ Ⅎ _ x C
10 9 nfcrii ⊢ w ∈ C → ∀ x w ∈ C