Theorem mapprop

Description: An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019) (Proof shortened by AV, 2-Jun-2024)

	Ref	Expression
Hypothesis	mapprop.f	⊢ 𝐹 = { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ }
Assertion	mapprop	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊 ) ) → 𝐹 ∈ ( 𝑅 ↑m { 𝑋 , 𝑌 } ) )

Proof

Step	Hyp	Ref	Expression
1		mapprop.f	⊢ 𝐹 = { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ }
2		simp3r	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊 ) ) → 𝑅 ∈ 𝑊 )
3		simpl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅 ) → 𝑋 ∈ 𝑉 )
4		simpl	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅 ) → 𝑌 ∈ 𝑉 )
5		simpl	⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊 ) → 𝑋 ≠ 𝑌 )
6	3 4 5	3anim123i	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ≠ 𝑌 ) )
7		simpr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅 ) → 𝐴 ∈ 𝑅 )
8		simpr	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅 ) → 𝐵 ∈ 𝑅 )
9	7 8	anim12i	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅 ) ) → ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) )
10	9	3adant3	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊 ) ) → ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) )
11		fprmappr	⊢ ( ( 𝑅 ∈ 𝑊 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) ) → { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∈ ( 𝑅 ↑m { 𝑋 , 𝑌 } ) )
12	2 6 10 11	syl3anc	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊 ) ) → { ⟨ 𝑋 , 𝐴 ⟩ , ⟨ 𝑌 , 𝐵 ⟩ } ∈ ( 𝑅 ↑m { 𝑋 , 𝑌 } ) )
13	1 12	eqeltrid	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑅 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑅 ∈ 𝑊 ) ) → 𝐹 ∈ ( 𝑅 ↑m { 𝑋 , 𝑌 } ) )