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 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
bnj1307.2 ( 𝑤𝐵 → ∀ 𝑥 𝑤𝐵 )
Assertion bnj1307 ( 𝑤𝐶 → ∀ 𝑥 𝑤𝐶 )

Proof

Step Hyp Ref Expression
1 bnj1307.1 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
2 bnj1307.2 ( 𝑤𝐵 → ∀ 𝑥 𝑤𝐵 )
3 2 nfcii 𝑥 𝐵
4 nfv 𝑥 𝑓 Fn 𝑑
5 nfra1 𝑥𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 )
6 4 5 nfan 𝑥 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) )
7 3 6 nfrex 𝑥𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) )
8 7 nfab 𝑥 { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
9 1 8 nfcxfr 𝑥 𝐶
10 9 nfcrii ( 𝑤𝐶 → ∀ 𝑥 𝑤𝐶 )