Theorem fprmappr

Description: A function with a domain of two elements as element of the mapping operator applied to a pair. (Contributed by AV, 20-May-2024)

	Ref	Expression
Assertion	fprmappr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ∈ ( 𝑋 ↑m { 𝐴 , 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		3simpa	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ) )
2	1	adantr	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ) )
3		simpr	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) )
4		simpl3	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐴 ≠ 𝐵 )
5		fprg	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } )
6	2 3 4 5	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } )
7		prssi	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) → { 𝐶 , 𝐷 } ⊆ 𝑋 )
8	7	adantl	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → { 𝐶 , 𝐷 } ⊆ 𝑋 )
9	6 8	fssd	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ 𝑋 )
10	9	3adant1	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ 𝑋 )
11		simp1	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝑋 ∈ 𝑉 )
12		prex	⊢ { 𝐴 , 𝐵 } ∈ V
13	12	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → { 𝐴 , 𝐵 } ∈ V )
14	11 13	elmapd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ∈ ( 𝑋 ↑m { 𝐴 , 𝐵 } ) ↔ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ 𝑋 ) )
15	10 14	mpbird	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ∈ ( 𝑋 ↑m { 𝐴 , 𝐵 } ) )