# Metamath Proof Explorer

## Theorem fnpr2ob

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

Ref Expression
Assertion fnpr2ob ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)↔\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}$

### Proof

Step Hyp Ref Expression
1 fnpr2o ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}$
2 0ex ${⊢}\varnothing \in \mathrm{V}$
3 2 prid1 ${⊢}\varnothing \in \left\{\varnothing ,{1}_{𝑜}\right\}$
4 df2o3 ${⊢}{2}_{𝑜}=\left\{\varnothing ,{1}_{𝑜}\right\}$
5 3 4 eleqtrri ${⊢}\varnothing \in {2}_{𝑜}$
6 fndm ${⊢}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}\to \mathrm{dom}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}={2}_{𝑜}$
7 5 6 eleqtrrid ${⊢}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}\to \varnothing \in \mathrm{dom}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}$
8 2 eldm2 ${⊢}\varnothing \in \mathrm{dom}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}↔\exists {k}\phantom{\rule{.4em}{0ex}}⟨\varnothing ,{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}$
9 7 8 sylib ${⊢}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}\to \exists {k}\phantom{\rule{.4em}{0ex}}⟨\varnothing ,{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}$
10 1n0 ${⊢}{1}_{𝑜}\ne \varnothing$
11 10 nesymi ${⊢}¬\varnothing ={1}_{𝑜}$
12 vex ${⊢}{k}\in \mathrm{V}$
13 2 12 opth1 ${⊢}⟨\varnothing ,{k}⟩=⟨{1}_{𝑜},{B}⟩\to \varnothing ={1}_{𝑜}$
14 11 13 mto ${⊢}¬⟨\varnothing ,{k}⟩=⟨{1}_{𝑜},{B}⟩$
15 elpri ${⊢}⟨\varnothing ,{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to \left(⟨\varnothing ,{k}⟩=⟨\varnothing ,{A}⟩\vee ⟨\varnothing ,{k}⟩=⟨{1}_{𝑜},{B}⟩\right)$
16 orel2 ${⊢}¬⟨\varnothing ,{k}⟩=⟨{1}_{𝑜},{B}⟩\to \left(\left(⟨\varnothing ,{k}⟩=⟨\varnothing ,{A}⟩\vee ⟨\varnothing ,{k}⟩=⟨{1}_{𝑜},{B}⟩\right)\to ⟨\varnothing ,{k}⟩=⟨\varnothing ,{A}⟩\right)$
17 14 15 16 mpsyl ${⊢}⟨\varnothing ,{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to ⟨\varnothing ,{k}⟩=⟨\varnothing ,{A}⟩$
18 2 12 opth ${⊢}⟨\varnothing ,{k}⟩=⟨\varnothing ,{A}⟩↔\left(\varnothing =\varnothing \wedge {k}={A}\right)$
19 17 18 sylib ${⊢}⟨\varnothing ,{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to \left(\varnothing =\varnothing \wedge {k}={A}\right)$
20 19 simprd ${⊢}⟨\varnothing ,{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to {k}={A}$
21 20 eximi ${⊢}\exists {k}\phantom{\rule{.4em}{0ex}}⟨\varnothing ,{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to \exists {k}\phantom{\rule{.4em}{0ex}}{k}={A}$
22 isset ${⊢}{A}\in \mathrm{V}↔\exists {k}\phantom{\rule{.4em}{0ex}}{k}={A}$
23 21 22 sylibr ${⊢}\exists {k}\phantom{\rule{.4em}{0ex}}⟨\varnothing ,{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to {A}\in \mathrm{V}$
24 9 23 syl ${⊢}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}\to {A}\in \mathrm{V}$
25 1oex ${⊢}{1}_{𝑜}\in \mathrm{V}$
26 25 prid2 ${⊢}{1}_{𝑜}\in \left\{\varnothing ,{1}_{𝑜}\right\}$
27 26 4 eleqtrri ${⊢}{1}_{𝑜}\in {2}_{𝑜}$
28 27 6 eleqtrrid ${⊢}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}\to {1}_{𝑜}\in \mathrm{dom}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}$
29 25 eldm2 ${⊢}{1}_{𝑜}\in \mathrm{dom}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}↔\exists {k}\phantom{\rule{.4em}{0ex}}⟨{1}_{𝑜},{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}$
30 28 29 sylib ${⊢}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}\to \exists {k}\phantom{\rule{.4em}{0ex}}⟨{1}_{𝑜},{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}$
31 10 neii ${⊢}¬{1}_{𝑜}=\varnothing$
32 25 12 opth1 ${⊢}⟨{1}_{𝑜},{k}⟩=⟨\varnothing ,{A}⟩\to {1}_{𝑜}=\varnothing$
33 31 32 mto ${⊢}¬⟨{1}_{𝑜},{k}⟩=⟨\varnothing ,{A}⟩$
34 elpri ${⊢}⟨{1}_{𝑜},{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to \left(⟨{1}_{𝑜},{k}⟩=⟨\varnothing ,{A}⟩\vee ⟨{1}_{𝑜},{k}⟩=⟨{1}_{𝑜},{B}⟩\right)$
35 34 orcomd ${⊢}⟨{1}_{𝑜},{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to \left(⟨{1}_{𝑜},{k}⟩=⟨{1}_{𝑜},{B}⟩\vee ⟨{1}_{𝑜},{k}⟩=⟨\varnothing ,{A}⟩\right)$
36 orel2 ${⊢}¬⟨{1}_{𝑜},{k}⟩=⟨\varnothing ,{A}⟩\to \left(\left(⟨{1}_{𝑜},{k}⟩=⟨{1}_{𝑜},{B}⟩\vee ⟨{1}_{𝑜},{k}⟩=⟨\varnothing ,{A}⟩\right)\to ⟨{1}_{𝑜},{k}⟩=⟨{1}_{𝑜},{B}⟩\right)$
37 33 35 36 mpsyl ${⊢}⟨{1}_{𝑜},{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to ⟨{1}_{𝑜},{k}⟩=⟨{1}_{𝑜},{B}⟩$
38 25 12 opth ${⊢}⟨{1}_{𝑜},{k}⟩=⟨{1}_{𝑜},{B}⟩↔\left({1}_{𝑜}={1}_{𝑜}\wedge {k}={B}\right)$
39 37 38 sylib ${⊢}⟨{1}_{𝑜},{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to \left({1}_{𝑜}={1}_{𝑜}\wedge {k}={B}\right)$
40 39 simprd ${⊢}⟨{1}_{𝑜},{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to {k}={B}$
41 40 eximi ${⊢}\exists {k}\phantom{\rule{.4em}{0ex}}⟨{1}_{𝑜},{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to \exists {k}\phantom{\rule{.4em}{0ex}}{k}={B}$
42 isset ${⊢}{B}\in \mathrm{V}↔\exists {k}\phantom{\rule{.4em}{0ex}}{k}={B}$
43 41 42 sylibr ${⊢}\exists {k}\phantom{\rule{.4em}{0ex}}⟨{1}_{𝑜},{k}⟩\in \left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}\to {B}\in \mathrm{V}$
44 30 43 syl ${⊢}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}\to {B}\in \mathrm{V}$
45 24 44 jca ${⊢}\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
46 1 45 impbii ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)↔\left\{⟨\varnothing ,{A}⟩,⟨{1}_{𝑜},{B}⟩\right\}Fn{2}_{𝑜}$