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 𝑜 → ∅ A 1 𝑜 B ⁡ C = if C = ∅ A B

Proof

Step Hyp Ref Expression
1 fvpr0o ⊢ A ∈ V → ∅ A 1 𝑜 B ⁡ ∅ = A
2 1 3ad2ant1 ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ 2 𝑜 → ∅ A 1 𝑜 B ⁡ ∅ = A
3 2 adantr ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ 2 𝑜 ∧ C = ∅ → ∅ A 1 𝑜 B ⁡ ∅ = A
4 simpr ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ 2 𝑜 ∧ C = ∅ → C = ∅
5 4 fveq2d ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ 2 𝑜 ∧ C = ∅ → ∅ A 1 𝑜 B ⁡ C = ∅ A 1 𝑜 B ⁡ ∅
6 4 iftrued ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ 2 𝑜 ∧ C = ∅ → if C = ∅ A B = A
7 3 5 6 3eqtr4d ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ 2 𝑜 ∧ C = ∅ → ∅ A 1 𝑜 B ⁡ C = if C = ∅ A B
8 fvpr1o ⊢ B ∈ W → ∅ A 1 𝑜 B ⁡ 1 𝑜 = B
9 8 3ad2ant2 ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ 2 𝑜 → ∅ A 1 𝑜 B ⁡ 1 𝑜 = B
10 9 adantr ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ 2 𝑜 ∧ C = 1 𝑜 → ∅ A 1 𝑜 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 𝑜 → ∅ A 1 𝑜 B ⁡ C = ∅ A 1 𝑜 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 𝑜 → if C = ∅ A B = B
18 10 12 17 3eqtr4d ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ 2 𝑜 ∧ C = 1 𝑜 → ∅ A 1 𝑜 B ⁡ C = if C = ∅ A B
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 𝑜 → ∅ A 1 𝑜 B ⁡ C = if C = ∅ A B