Metamath Proof Explorer

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 ⊢ X ∈ V ∧ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → A C B D ∈ X A B

Proof

Step Hyp Ref Expression
1 3simpa ⊢ A ∈ U ∧ B ∈ W ∧ A ≠ B → A ∈ U ∧ B ∈ W
2 1 adantr ⊢ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → A ∈ U ∧ B ∈ W
3 simpr ⊢ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → C ∈ X ∧ D ∈ X
4 simpl3 ⊢ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → A ≠ B
5 fprg ⊢ A ∈ U ∧ B ∈ W ∧ C ∈ X ∧ D ∈ X ∧ A ≠ B → A C B D : A B ⟶ C D
6 2 3 4 5 syl3anc ⊢ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → A C B D : A B ⟶ C D
7 prssi ⊢ C ∈ X ∧ D ∈ X → C D ⊆ X
8 7 adantl ⊢ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → C D ⊆ X
9 6 8 fssd ⊢ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → A C B D : A B ⟶ X
10 9 3adant1 ⊢ X ∈ V ∧ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → A C B D : A B ⟶ X
11 simp1 ⊢ X ∈ V ∧ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → X ∈ V
12 prex ⊢ A B ∈ V
13 12 a1i ⊢ X ∈ V ∧ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → A B ∈ V
14 11 13 elmapd ⊢ X ∈ V ∧ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → A C B D ∈ X A B ↔ A C B D : A B ⟶ X
15 10 14 mpbird ⊢ X ∈ V ∧ A ∈ U ∧ B ∈ W ∧ A ≠ B ∧ C ∈ X ∧ D ∈ X → A C B D ∈ X A B