fvprif

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

		Ref	Expression
	Assertion	fvprif	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝐶 ) = if ( 𝐶 = ∅ , 𝐴 , 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fvpr0o	⊢ ( 𝐴 ∈ 𝑉 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )
3	2	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = ∅ ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )
4		simpr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = ∅ ) → 𝐶 = ∅ )
5	4	fveq2d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = ∅ ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝐶 ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ ∅ ) )
6	4	iftrued	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = ∅ ) → if ( 𝐶 = ∅ , 𝐴 , 𝐵 ) = 𝐴 )
7	3 5 6	3eqtr4d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = ∅ ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝐶 ) = if ( 𝐶 = ∅ , 𝐴 , 𝐵 ) )
8		fvpr1o	⊢ ( 𝐵 ∈ 𝑊 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) = 𝐵 )
9	8	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) = 𝐵 )
10	9	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = 1_o ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) = 𝐵 )
11		simpr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = 1_o ) → 𝐶 = 1_o )
12	11	fveq2d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = 1_o ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝐶 ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 1_o ) )
13		1n0	⊢ 1_o ≠ ∅
14	13	neii	⊢ ¬ 1_o = ∅
15	11	eqeq1d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = 1_o ) → ( 𝐶 = ∅ ↔ 1_o = ∅ ) )
16	14 15	mtbiri	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = 1_o ) → ¬ 𝐶 = ∅ )
17	16	iffalsed	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = 1_o ) → if ( 𝐶 = ∅ , 𝐴 , 𝐵 ) = 𝐵 )
18	10 12 17	3eqtr4d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) ∧ 𝐶 = 1_o ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝐶 ) = if ( 𝐶 = ∅ , 𝐴 , 𝐵 ) )
19		elpri	⊢ ( 𝐶 ∈ { ∅ , 1_o } → ( 𝐶 = ∅ ∨ 𝐶 = 1_o ) )
20		df2o3	⊢ 2_o = { ∅ , 1_o }
21	19 20	eleq2s	⊢ ( 𝐶 ∈ 2_o → ( 𝐶 = ∅ ∨ 𝐶 = 1_o ) )
22	21	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) → ( 𝐶 = ∅ ∨ 𝐶 = 1_o ) )
23	7 18 22	mpjaodan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2_o ) → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1_o , 𝐵 ⟩ } ‘ 𝐶 ) = if ( 𝐶 = ∅ , 𝐴 , 𝐵 ) )

Metamath Proof Explorer

Theorem fvprif

Proof