# Metamath Proof Explorer

## Theorem xpscf

Description: Equivalent condition for the pair function to be a proper function on A . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xpscf ${⊢}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}:{2}_{𝑜}⟶{A}↔\left({X}\in {A}\wedge {Y}\in {A}\right)$

### Proof

Step Hyp Ref Expression
1 ifid ${⊢}if\left({k}=\varnothing ,{A},{A}\right)={A}$
2 1 eleq2i ${⊢}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in if\left({k}=\varnothing ,{A},{A}\right)↔\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in {A}$
3 2 ralbii ${⊢}\forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in if\left({k}=\varnothing ,{A},{A}\right)↔\forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in {A}$
4 3 anbi2i ${⊢}\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\wedge \forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in if\left({k}=\varnothing ,{A},{A}\right)\right)↔\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\wedge \forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in {A}\right)$
5 df-3an ${⊢}\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \mathrm{V}\wedge \left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\wedge \forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in if\left({k}=\varnothing ,{A},{A}\right)\right)↔\left(\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \mathrm{V}\wedge \left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\right)\wedge \forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in if\left({k}=\varnothing ,{A},{A}\right)\right)$
6 elixp2 ${⊢}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{A}\right)↔\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \mathrm{V}\wedge \left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\wedge \forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in if\left({k}=\varnothing ,{A},{A}\right)\right)$
7 2onn ${⊢}{2}_{𝑜}\in \mathrm{\omega }$
8 fnex ${⊢}\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\wedge {2}_{𝑜}\in \mathrm{\omega }\right)\to \left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \mathrm{V}$
9 7 8 mpan2 ${⊢}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\to \left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \mathrm{V}$
10 9 pm4.71ri ${⊢}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}↔\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \mathrm{V}\wedge \left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\right)$
11 10 anbi1i ${⊢}\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\wedge \forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in if\left({k}=\varnothing ,{A},{A}\right)\right)↔\left(\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \mathrm{V}\wedge \left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\right)\wedge \forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in if\left({k}=\varnothing ,{A},{A}\right)\right)$
12 5 6 11 3bitr4i ${⊢}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{A}\right)↔\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\wedge \forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in if\left({k}=\varnothing ,{A},{A}\right)\right)$
13 ffnfv ${⊢}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}:{2}_{𝑜}⟶{A}↔\left(\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}Fn{2}_{𝑜}\wedge \forall {k}\in {2}_{𝑜}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\left({k}\right)\in {A}\right)$
14 4 12 13 3bitr4i ${⊢}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{A}\right)↔\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}:{2}_{𝑜}⟶{A}$
15 xpsfrnel2 ${⊢}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{A}\right)↔\left({X}\in {A}\wedge {Y}\in {A}\right)$
16 14 15 bitr3i ${⊢}\left\{⟨\varnothing ,{X}⟩,⟨{1}_{𝑜},{Y}⟩\right\}:{2}_{𝑜}⟶{A}↔\left({X}\in {A}\wedge {Y}\in {A}\right)$