Theorem fnpr2o

Description: Function with a domain of 2o . (Contributed by Jim Kingdon, 25-Sep-2023)

	Ref	Expression
Assertion	fnpr2o	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o )

Proof

Step	Hyp	Ref	Expression
1		peano1	⊢ ∅ ∈ ω
2	1	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∅ ∈ ω )
3		1onn	⊢ 1o ∈ ω
4	3	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 1o ∈ ω )
5		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 )
6		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
7		1n0	⊢ 1o ≠ ∅
8	7	necomi	⊢ ∅ ≠ 1o
9	8	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∅ ≠ 1o )
10		fnprg	⊢ ( ( ( ∅ ∈ ω ∧ 1o ∈ ω ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ∅ ≠ 1o ) → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn { ∅ , 1o } )
11	2 4 5 6 9 10	syl221anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn { ∅ , 1o } )
12		df2o3	⊢ 2o = { ∅ , 1o }
13	12	fneq2i	⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o ↔ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn { ∅ , 1o } )
14	11 13	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o )