Metamath Proof Explorer

Theorem prproe

Description: For an element of a proper unordered pair of elements of a class V , there is another (different) element of the class V which is an element of the proper pair. (Contributed by AV, 18-Dec-2021)

Ref Expression
Assertion prproe ( ( 𝐶 ∈ { 𝐴 , 𝐵 } ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝐶 } ) 𝑣 ∈ { 𝐴 , 𝐵 } )

Proof

Step Hyp Ref Expression
1 elpri ⊢ ( 𝐶 ∈ { 𝐴 , 𝐵 } → ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) )
2 simprrr ⊢ ( ( 𝐶 = 𝐴 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) → 𝐵 ∈ 𝑉 )
3 necom ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
4 neeq2 ⊢ ( 𝐴 = 𝐶 → ( 𝐵 ≠ 𝐴 ↔ 𝐵 ≠ 𝐶 ) )
5 4 eqcoms ⊢ ( 𝐶 = 𝐴 → ( 𝐵 ≠ 𝐴 ↔ 𝐵 ≠ 𝐶 ) )
6 5 biimpcd ⊢ ( 𝐵 ≠ 𝐴 → ( 𝐶 = 𝐴 → 𝐵 ≠ 𝐶 ) )
7 3 6 sylbi ⊢ ( 𝐴 ≠ 𝐵 → ( 𝐶 = 𝐴 → 𝐵 ≠ 𝐶 ) )
8 7 adantr ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐶 = 𝐴 → 𝐵 ≠ 𝐶 ) )
9 8 impcom ⊢ ( ( 𝐶 = 𝐴 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) → 𝐵 ≠ 𝐶 )
10 eldifsn ⊢ ( 𝐵 ∈ ( 𝑉 ∖ { 𝐶 } ) ↔ ( 𝐵 ∈ 𝑉 ∧ 𝐵 ≠ 𝐶 ) )
11 2 9 10 sylanbrc ⊢ ( ( 𝐶 = 𝐴 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) → 𝐵 ∈ ( 𝑉 ∖ { 𝐶 } ) )
12 eleq1 ⊢ ( 𝑣 = 𝐵 → ( 𝑣 ∈ { 𝐴 , 𝐵 } ↔ 𝐵 ∈ { 𝐴 , 𝐵 } ) )
13 12 adantl ⊢ ( ( ( 𝐶 = 𝐴 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ∧ 𝑣 = 𝐵 ) → ( 𝑣 ∈ { 𝐴 , 𝐵 } ↔ 𝐵 ∈ { 𝐴 , 𝐵 } ) )
14 prid2g ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ { 𝐴 , 𝐵 } )
15 14 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
16 15 adantl ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
17 16 adantl ⊢ ( ( 𝐶 = 𝐴 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
18 11 13 17 rspcedvd ⊢ ( ( 𝐶 = 𝐴 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝐶 } ) 𝑣 ∈ { 𝐴 , 𝐵 } )
19 18 ex ⊢ ( 𝐶 = 𝐴 → ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝐶 } ) 𝑣 ∈ { 𝐴 , 𝐵 } ) )
20 simprrl ⊢ ( ( 𝐶 = 𝐵 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) → 𝐴 ∈ 𝑉 )
21 neeq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶 ) )
22 21 eqcoms ⊢ ( 𝐶 = 𝐵 → ( 𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶 ) )
23 22 biimpcd ⊢ ( 𝐴 ≠ 𝐵 → ( 𝐶 = 𝐵 → 𝐴 ≠ 𝐶 ) )
24 23 adantr ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐶 = 𝐵 → 𝐴 ≠ 𝐶 ) )
25 24 impcom ⊢ ( ( 𝐶 = 𝐵 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) → 𝐴 ≠ 𝐶 )
26 eldifsn ⊢ ( 𝐴 ∈ ( 𝑉 ∖ { 𝐶 } ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) )
27 20 25 26 sylanbrc ⊢ ( ( 𝐶 = 𝐵 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) → 𝐴 ∈ ( 𝑉 ∖ { 𝐶 } ) )
28 eleq1 ⊢ ( 𝑣 = 𝐴 → ( 𝑣 ∈ { 𝐴 , 𝐵 } ↔ 𝐴 ∈ { 𝐴 , 𝐵 } ) )
29 28 adantl ⊢ ( ( ( 𝐶 = 𝐵 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) ∧ 𝑣 = 𝐴 ) → ( 𝑣 ∈ { 𝐴 , 𝐵 } ↔ 𝐴 ∈ { 𝐴 , 𝐵 } ) )
30 prid1g ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 } )
31 30 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
32 31 adantl ⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
33 32 adantl ⊢ ( ( 𝐶 = 𝐵 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
34 27 29 33 rspcedvd ⊢ ( ( 𝐶 = 𝐵 ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝐶 } ) 𝑣 ∈ { 𝐴 , 𝐵 } )
35 34 ex ⊢ ( 𝐶 = 𝐵 → ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝐶 } ) 𝑣 ∈ { 𝐴 , 𝐵 } ) )
36 19 35 jaoi ⊢ ( ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) → ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝐶 } ) 𝑣 ∈ { 𝐴 , 𝐵 } ) )
37 1 36 syl ⊢ ( 𝐶 ∈ { 𝐴 , 𝐵 } → ( ( 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝐶 } ) 𝑣 ∈ { 𝐴 , 𝐵 } ) )
38 37 3impib ⊢ ( ( 𝐶 ∈ { 𝐴 , 𝐵 } ∧ 𝐴 ≠ 𝐵 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ∃ 𝑣 ∈ ( 𝑉 ∖ { 𝐶 } ) 𝑣 ∈ { 𝐴 , 𝐵 } )