Metamath Proof Explorer

Theorem prsprel

Description: The elements of a pair from the set of all unordered pairs over a given set V are elements of the set V . (Contributed by AV, 22-Nov-2021)

Ref Expression
Assertion prsprel ( ( { 𝑋 , 𝑌 } ∈ ( Pairs ‘ 𝑉 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 sprel ⊢ ( { 𝑋 , 𝑌 } ∈ ( Pairs ‘ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } )
2 preq12bg ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } ↔ ( ( 𝑋 = 𝑎 ∧ 𝑌 = 𝑏 ) ∨ ( 𝑋 = 𝑏 ∧ 𝑌 = 𝑎 ) ) ) )
3 eleq1 ⊢ ( 𝑎 = 𝑋 → ( 𝑎 ∈ 𝑉 ↔ 𝑋 ∈ 𝑉 ) )
4 3 eqcoms ⊢ ( 𝑋 = 𝑎 → ( 𝑎 ∈ 𝑉 ↔ 𝑋 ∈ 𝑉 ) )
5 eleq1 ⊢ ( 𝑏 = 𝑌 → ( 𝑏 ∈ 𝑉 ↔ 𝑌 ∈ 𝑉 ) )
6 5 eqcoms ⊢ ( 𝑌 = 𝑏 → ( 𝑏 ∈ 𝑉 ↔ 𝑌 ∈ 𝑉 ) )
7 4 6 bi2anan9 ⊢ ( ( 𝑋 = 𝑎 ∧ 𝑌 = 𝑏 ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
8 7 biimpd ⊢ ( ( 𝑋 = 𝑎 ∧ 𝑌 = 𝑏 ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
9 eleq1 ⊢ ( 𝑏 = 𝑋 → ( 𝑏 ∈ 𝑉 ↔ 𝑋 ∈ 𝑉 ) )
10 9 eqcoms ⊢ ( 𝑋 = 𝑏 → ( 𝑏 ∈ 𝑉 ↔ 𝑋 ∈ 𝑉 ) )
11 eleq1 ⊢ ( 𝑎 = 𝑌 → ( 𝑎 ∈ 𝑉 ↔ 𝑌 ∈ 𝑉 ) )
12 11 eqcoms ⊢ ( 𝑌 = 𝑎 → ( 𝑎 ∈ 𝑉 ↔ 𝑌 ∈ 𝑉 ) )
13 10 12 bi2anan9 ⊢ ( ( 𝑋 = 𝑏 ∧ 𝑌 = 𝑎 ) → ( ( 𝑏 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉 ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
14 13 biimpd ⊢ ( ( 𝑋 = 𝑏 ∧ 𝑌 = 𝑎 ) → ( ( 𝑏 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
15 14 ancomsd ⊢ ( ( 𝑋 = 𝑏 ∧ 𝑌 = 𝑎 ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
16 8 15 jaoi ⊢ ( ( ( 𝑋 = 𝑎 ∧ 𝑌 = 𝑏 ) ∨ ( 𝑋 = 𝑏 ∧ 𝑌 = 𝑎 ) ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
17 16 com12 ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( ( 𝑋 = 𝑎 ∧ 𝑌 = 𝑏 ) ∨ ( 𝑋 = 𝑏 ∧ 𝑌 = 𝑎 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
18 17 adantl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( ( 𝑋 = 𝑎 ∧ 𝑌 = 𝑏 ) ∨ ( 𝑋 = 𝑏 ∧ 𝑌 = 𝑎 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
19 2 18 sylbid ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
20 19 expcom ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) → ( { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ) )
21 20 com23 ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } → ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ) )
22 21 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 { 𝑋 , 𝑌 } = { 𝑎 , 𝑏 } → ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
23 1 22 syl ⊢ ( { 𝑋 , 𝑌 } ∈ ( Pairs ‘ 𝑉 ) → ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) )
24 23 imp ⊢ ( ( { 𝑋 , 𝑌 } ∈ ( Pairs ‘ 𝑉 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )