up1st2ndb

Description: Combine/separate parts in the universal property predicate. (Contributed by Zhi Wang, 23-Oct-2025)

		Ref	Expression
	Hypothesis	up1st2ndr.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
	Assertion	up1st2ndb	⊢ ( 𝜑 → ( 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 ↔ 𝑋 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 ) )

Step	Hyp	Ref	Expression
1		up1st2ndr.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
2		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 ) → 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 )
3	2	up1st2nd	⊢ ( ( 𝜑 ∧ 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 ) → 𝑋 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 )
4	1	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 ) → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 ) → 𝑋 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 )
6	4 5	up1st2ndr	⊢ ( ( 𝜑 ∧ 𝑋 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 ) → 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 )
7	3 6	impbida	⊢ ( 𝜑 → ( 𝑋 ( 𝐹 ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 ↔ 𝑋 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 ) )

Metamath Proof Explorer