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

Metamath Proof Explorer

Theorem fnpr2ob

Description: Biconditional version of fnpr2o . (Contributed by Jim Kingdon, 27-Sep-2023)

Ref Expression
Assertion fnpr2ob ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o )

Proof

Step Hyp Ref Expression
1 fnpr2o ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o )
2 0ex ⊢ ∅ ∈ V
3 2 prid1 ⊢ ∅ ∈ { ∅ , 1o }
4 df2o3 ⊢ 2o = { ∅ , 1o }
5 3 4 eleqtrri ⊢ ∅ ∈ 2o
6 fndm ⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → dom { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } = 2o )
7 5 6 eleqtrrid ⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → ∅ ∈ dom { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
8 2 eldm2 ⊢ ( ∅ ∈ dom { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ↔ ∃ 𝑘 ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
9 7 8 sylib ⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → ∃ 𝑘 ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
10 1n0 ⊢ 1o ≠ ∅
11 10 nesymi ⊢ ¬ ∅ = 1o
12 vex ⊢ 𝑘 ∈ V
13 2 12 opth1 ⊢ ( ⟨ ∅ , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ → ∅ = 1o )
14 11 13 mto ⊢ ¬ ⟨ ∅ , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩
15 elpri ⊢ ( ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ⟨ ∅ , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ∨ ⟨ ∅ , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ) )
16 orel2 ⊢ ( ¬ ⟨ ∅ , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ → ( ( ⟨ ∅ , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ∨ ⟨ ∅ , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ) → ⟨ ∅ , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ) )
17 14 15 16 mpsyl ⊢ ( ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ⟨ ∅ , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ )
18 2 12 opth ⊢ ( ⟨ ∅ , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ↔ ( ∅ = ∅ ∧ 𝑘 = 𝐴 ) )
19 17 18 sylib ⊢ ( ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ∅ = ∅ ∧ 𝑘 = 𝐴 ) )
20 19 simprd ⊢ ( ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → 𝑘 = 𝐴 )
21 20 eximi ⊢ ( ∃ 𝑘 ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ∃ 𝑘 𝑘 = 𝐴 )
22 isset ⊢ ( 𝐴 ∈ V ↔ ∃ 𝑘 𝑘 = 𝐴 )
23 21 22 sylibr ⊢ ( ∃ 𝑘 ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → 𝐴 ∈ V )
24 9 23 syl ⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → 𝐴 ∈ V )
25 1oex ⊢ 1o ∈ V
26 25 prid2 ⊢ 1o ∈ { ∅ , 1o }
27 26 4 eleqtrri ⊢ 1o ∈ 2o
28 27 6 eleqtrrid ⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → 1o ∈ dom { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
29 25 eldm2 ⊢ ( 1o ∈ dom { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ↔ ∃ 𝑘 ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
30 28 29 sylib ⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → ∃ 𝑘 ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
31 10 neii ⊢ ¬ 1o = ∅
32 25 12 opth1 ⊢ ( ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ → 1o = ∅ )
33 31 32 mto ⊢ ¬ ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩
34 elpri ⊢ ( ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ∨ ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ) )
35 34 orcomd ⊢ ( ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ∨ ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ) )
36 orel2 ⊢ ( ¬ ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ → ( ( ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ∨ ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ) → ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ) )
37 33 35 36 mpsyl ⊢ ( ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ )
38 25 12 opth ⊢ ( ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ↔ ( 1o = 1o ∧ 𝑘 = 𝐵 ) )
39 37 38 sylib ⊢ ( ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( 1o = 1o ∧ 𝑘 = 𝐵 ) )
40 39 simprd ⊢ ( ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → 𝑘 = 𝐵 )
41 40 eximi ⊢ ( ∃ 𝑘 ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ∃ 𝑘 𝑘 = 𝐵 )
42 isset ⊢ ( 𝐵 ∈ V ↔ ∃ 𝑘 𝑘 = 𝐵 )
43 41 42 sylibr ⊢ ( ∃ 𝑘 ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → 𝐵 ∈ V )
44 30 43 syl ⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → 𝐵 ∈ V )
45 24 44 jca ⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
46 1 45 impbii ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o )