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

Metamath Proof Explorer

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 )