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 )