Theorem bj-mpomptALT

Description: Alternate proof of mpompt . (Contributed by BJ, 30-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bj-mpomptALT.1	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐶 = 𝐷 )
Assertion	bj-mpomptALT	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		bj-mpomptALT.1	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐶 = 𝐷 )
2		elxp2	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
3	2	anbi1i	⊢ ( ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑡 = 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) )
4		r19.41v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) )
5		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) )
6	1	eqeq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑡 = 𝐶 ↔ 𝑡 = 𝐷 ) )
7	6	pm5.32i	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐷 ) )
8	7	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐷 ) )
9	5 8	bitr3i	⊢ ( ( ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐷 ) )
10	9	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐷 ) )
11	3 4 10	3bitr2i	⊢ ( ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑡 = 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐷 ) )
12	11	opabbii	⊢ { ⟨ 𝑧 , 𝑡 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑡 = 𝐶 ) } = { ⟨ 𝑧 , 𝑡 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐷 ) }
13		df-mpt	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐶 ) = { ⟨ 𝑧 , 𝑡 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑡 = 𝐶 ) }
14		bj-dfmpoa	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) = { ⟨ 𝑧 , 𝑡 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑡 = 𝐷 ) }
15	12 13 14	3eqtr4i	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 )