Metamath Proof Explorer

Theorem fvprif

Description: The value of the pair function at an element of 2o . (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion fvprif ⊢A∈V∧B∈W∧C∈2𝑜→∅A1𝑜B⁡C=ifC=∅AB

Proof

Step Hyp Ref Expression
1 fvpr0o ⊢A∈V→∅A1𝑜B⁡∅=A
2 1 3ad2ant1 ⊢A∈V∧B∈W∧C∈2𝑜→∅A1𝑜B⁡∅=A
3 2 adantr ⊢A∈V∧B∈W∧C∈2𝑜∧C=∅→∅A1𝑜B⁡∅=A
4 simpr ⊢A∈V∧B∈W∧C∈2𝑜∧C=∅→C=∅
5 4 fveq2d ⊢A∈V∧B∈W∧C∈2𝑜∧C=∅→∅A1𝑜B⁡C=∅A1𝑜B⁡∅
6 4 iftrued ⊢A∈V∧B∈W∧C∈2𝑜∧C=∅→ifC=∅AB=A
7 3 5 6 3eqtr4d ⊢A∈V∧B∈W∧C∈2𝑜∧C=∅→∅A1𝑜B⁡C=ifC=∅AB
8 fvpr1o ⊢B∈W→∅A1𝑜B⁡1𝑜=B
9 8 3ad2ant2 ⊢A∈V∧B∈W∧C∈2𝑜→∅A1𝑜B⁡1𝑜=B
10 9 adantr ⊢A∈V∧B∈W∧C∈2𝑜∧C=1𝑜→∅A1𝑜B⁡1𝑜=B
11 simpr ⊢A∈V∧B∈W∧C∈2𝑜∧C=1𝑜→C=1𝑜
12 11 fveq2d ⊢A∈V∧B∈W∧C∈2𝑜∧C=1𝑜→∅A1𝑜B⁡C=∅A1𝑜B⁡1𝑜
13 1n0 ⊢1𝑜≠∅
14 13 neii ⊢¬1𝑜=∅
15 11 eqeq1d ⊢A∈V∧B∈W∧C∈2𝑜∧C=1𝑜→C=∅↔1𝑜=∅
16 14 15 mtbiri ⊢A∈V∧B∈W∧C∈2𝑜∧C=1𝑜→¬C=∅
17 16 iffalsed ⊢A∈V∧B∈W∧C∈2𝑜∧C=1𝑜→ifC=∅AB=B
18 10 12 17 3eqtr4d ⊢A∈V∧B∈W∧C∈2𝑜∧C=1𝑜→∅A1𝑜B⁡C=ifC=∅AB
19 elpri ⊢C∈∅1𝑜→C=∅∨C=1𝑜
20 df2o3 ⊢2𝑜=∅1𝑜
21 19 20 eleq2s ⊢C∈2𝑜→C=∅∨C=1𝑜
22 21 3ad2ant3 ⊢A∈V∧B∈W∧C∈2𝑜→C=∅∨C=1𝑜
23 7 18 22 mpjaodan ⊢A∈V∧B∈W∧C∈2𝑜→∅A1𝑜B⁡C=ifC=∅AB