bnj900

Description: Technical lemma for bnj69 . 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	bnj900.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj900.4	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
Assertion	bnj900	⊢ ( 𝑓 ∈ 𝐵 → ∅ ∈ dom 𝑓 )

Proof

Step	Hyp	Ref	Expression
1		bnj900.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
2		bnj900.4	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
3	2	bnj1436	⊢ ( 𝑓 ∈ 𝐵 → ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4		simp1	⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → 𝑓 Fn 𝑛 )
5	4	reximi	⊢ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) → ∃ 𝑛 ∈ 𝐷 𝑓 Fn 𝑛 )
6		fndm	⊢ ( 𝑓 Fn 𝑛 → dom 𝑓 = 𝑛 )
7	6	reximi	⊢ ( ∃ 𝑛 ∈ 𝐷 𝑓 Fn 𝑛 → ∃ 𝑛 ∈ 𝐷 dom 𝑓 = 𝑛 )
8	3 5 7	3syl	⊢ ( 𝑓 ∈ 𝐵 → ∃ 𝑛 ∈ 𝐷 dom 𝑓 = 𝑛 )
9	8	bnj1196	⊢ ( 𝑓 ∈ 𝐵 → ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ dom 𝑓 = 𝑛 ) )
10		nfre1	⊢ Ⅎ 𝑛 ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 )
11	10	nfab	⊢ Ⅎ 𝑛 { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
12	2 11	nfcxfr	⊢ Ⅎ 𝑛 𝐵
13	12	nfcri	⊢ Ⅎ 𝑛 𝑓 ∈ 𝐵
14	13	19.37	⊢ ( ∃ 𝑛 ( 𝑓 ∈ 𝐵 → ( 𝑛 ∈ 𝐷 ∧ dom 𝑓 = 𝑛 ) ) ↔ ( 𝑓 ∈ 𝐵 → ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ dom 𝑓 = 𝑛 ) ) )
15	9 14	mpbir	⊢ ∃ 𝑛 ( 𝑓 ∈ 𝐵 → ( 𝑛 ∈ 𝐷 ∧ dom 𝑓 = 𝑛 ) )
16		nfv	⊢ Ⅎ 𝑛 ∅ ∈ dom 𝑓
17	13 16	nfim	⊢ Ⅎ 𝑛 ( 𝑓 ∈ 𝐵 → ∅ ∈ dom 𝑓 )
18	1	bnj529	⊢ ( 𝑛 ∈ 𝐷 → ∅ ∈ 𝑛 )
19		eleq2	⊢ ( dom 𝑓 = 𝑛 → ( ∅ ∈ dom 𝑓 ↔ ∅ ∈ 𝑛 ) )
20	19	biimparc	⊢ ( ( ∅ ∈ 𝑛 ∧ dom 𝑓 = 𝑛 ) → ∅ ∈ dom 𝑓 )
21	18 20	sylan	⊢ ( ( 𝑛 ∈ 𝐷 ∧ dom 𝑓 = 𝑛 ) → ∅ ∈ dom 𝑓 )
22	21	imim2i	⊢ ( ( 𝑓 ∈ 𝐵 → ( 𝑛 ∈ 𝐷 ∧ dom 𝑓 = 𝑛 ) ) → ( 𝑓 ∈ 𝐵 → ∅ ∈ dom 𝑓 ) )
23	17 22	exlimi	⊢ ( ∃ 𝑛 ( 𝑓 ∈ 𝐵 → ( 𝑛 ∈ 𝐷 ∧ dom 𝑓 = 𝑛 ) ) → ( 𝑓 ∈ 𝐵 → ∅ ∈ dom 𝑓 ) )
24	15 23	ax-mp	⊢ ( 𝑓 ∈ 𝐵 → ∅ ∈ dom 𝑓 )

Metamath Proof Explorer

Theorem bnj900

Proof