This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3elpr2eq

Description: If there are three elements in a proper unordered pair, and two of them are different from the third one, the two must be equal. (Contributed by AV, 19-Dec-2021)

Ref Expression
Assertion 3elpr2eq ( ( ( 𝑋 ∈ { 𝐴 , 𝐵 } ∧ 𝑌 ∈ { 𝐴 , 𝐵 } ∧ 𝑍 ∈ { 𝐴 , 𝐵 } ) ∧ ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) ) → 𝑌 = 𝑍 )

Proof

Step Hyp Ref Expression
1 elpri ⊢ ( 𝑋 ∈ { 𝐴 , 𝐵 } → ( 𝑋 = 𝐴 ∨ 𝑋 = 𝐵 ) )
2 elpri ⊢ ( 𝑌 ∈ { 𝐴 , 𝐵 } → ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) )
3 elpri ⊢ ( 𝑍 ∈ { 𝐴 , 𝐵 } → ( 𝑍 = 𝐴 ∨ 𝑍 = 𝐵 ) )
4 eqtr3 ⊢ ( ( 𝑍 = 𝐴 ∧ 𝑋 = 𝐴 ) → 𝑍 = 𝑋 )
5 eqneqall ⊢ ( 𝑍 = 𝑋 → ( 𝑍 ≠ 𝑋 → 𝑌 = 𝑍 ) )
6 4 5 syl ⊢ ( ( 𝑍 = 𝐴 ∧ 𝑋 = 𝐴 ) → ( 𝑍 ≠ 𝑋 → 𝑌 = 𝑍 ) )
7 6 adantld ⊢ ( ( 𝑍 = 𝐴 ∧ 𝑋 = 𝐴 ) → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) )
8 7 ex ⊢ ( 𝑍 = 𝐴 → ( 𝑋 = 𝐴 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) )
9 8 a1d ⊢ ( 𝑍 = 𝐴 → ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( 𝑋 = 𝐴 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
10 eqtr3 ⊢ ( ( 𝑌 = 𝐴 ∧ 𝑋 = 𝐴 ) → 𝑌 = 𝑋 )
11 eqneqall ⊢ ( 𝑌 = 𝑋 → ( 𝑌 ≠ 𝑋 → ( 𝑍 ≠ 𝑋 → 𝑌 = 𝑍 ) ) )
12 10 11 syl ⊢ ( ( 𝑌 = 𝐴 ∧ 𝑋 = 𝐴 ) → ( 𝑌 ≠ 𝑋 → ( 𝑍 ≠ 𝑋 → 𝑌 = 𝑍 ) ) )
13 12 impd ⊢ ( ( 𝑌 = 𝐴 ∧ 𝑋 = 𝐴 ) → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) )
14 13 ex ⊢ ( 𝑌 = 𝐴 → ( 𝑋 = 𝐴 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) )
15 14 a1d ⊢ ( 𝑌 = 𝐴 → ( 𝑍 = 𝐵 → ( 𝑋 = 𝐴 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
16 eqtr3 ⊢ ( ( 𝑌 = 𝐵 ∧ 𝑍 = 𝐵 ) → 𝑌 = 𝑍 )
17 16 2a1d ⊢ ( ( 𝑌 = 𝐵 ∧ 𝑍 = 𝐵 ) → ( 𝑋 = 𝐴 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) )
18 17 ex ⊢ ( 𝑌 = 𝐵 → ( 𝑍 = 𝐵 → ( 𝑋 = 𝐴 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
19 15 18 jaoi ⊢ ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( 𝑍 = 𝐵 → ( 𝑋 = 𝐴 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
20 19 com12 ⊢ ( 𝑍 = 𝐵 → ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( 𝑋 = 𝐴 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
21 9 20 jaoi ⊢ ( ( 𝑍 = 𝐴 ∨ 𝑍 = 𝐵 ) → ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( 𝑋 = 𝐴 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
22 21 com13 ⊢ ( 𝑋 = 𝐴 → ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( ( 𝑍 = 𝐴 ∨ 𝑍 = 𝐵 ) → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
23 eqtr3 ⊢ ( ( 𝑌 = 𝐴 ∧ 𝑍 = 𝐴 ) → 𝑌 = 𝑍 )
24 23 2a1d ⊢ ( ( 𝑌 = 𝐴 ∧ 𝑍 = 𝐴 ) → ( 𝑋 = 𝐵 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) )
25 24 ex ⊢ ( 𝑌 = 𝐴 → ( 𝑍 = 𝐴 → ( 𝑋 = 𝐵 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
26 eqtr3 ⊢ ( ( 𝑌 = 𝐵 ∧ 𝑋 = 𝐵 ) → 𝑌 = 𝑋 )
27 26 11 syl ⊢ ( ( 𝑌 = 𝐵 ∧ 𝑋 = 𝐵 ) → ( 𝑌 ≠ 𝑋 → ( 𝑍 ≠ 𝑋 → 𝑌 = 𝑍 ) ) )
28 27 impd ⊢ ( ( 𝑌 = 𝐵 ∧ 𝑋 = 𝐵 ) → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) )
29 28 ex ⊢ ( 𝑌 = 𝐵 → ( 𝑋 = 𝐵 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) )
30 29 a1d ⊢ ( 𝑌 = 𝐵 → ( 𝑍 = 𝐴 → ( 𝑋 = 𝐵 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
31 25 30 jaoi ⊢ ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( 𝑍 = 𝐴 → ( 𝑋 = 𝐵 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
32 31 com12 ⊢ ( 𝑍 = 𝐴 → ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( 𝑋 = 𝐵 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
33 eqtr3 ⊢ ( ( 𝑍 = 𝐵 ∧ 𝑋 = 𝐵 ) → 𝑍 = 𝑋 )
34 33 5 syl ⊢ ( ( 𝑍 = 𝐵 ∧ 𝑋 = 𝐵 ) → ( 𝑍 ≠ 𝑋 → 𝑌 = 𝑍 ) )
35 34 adantld ⊢ ( ( 𝑍 = 𝐵 ∧ 𝑋 = 𝐵 ) → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) )
36 35 ex ⊢ ( 𝑍 = 𝐵 → ( 𝑋 = 𝐵 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) )
37 36 a1d ⊢ ( 𝑍 = 𝐵 → ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( 𝑋 = 𝐵 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
38 32 37 jaoi ⊢ ( ( 𝑍 = 𝐴 ∨ 𝑍 = 𝐵 ) → ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( 𝑋 = 𝐵 → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
39 38 com13 ⊢ ( 𝑋 = 𝐵 → ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( ( 𝑍 = 𝐴 ∨ 𝑍 = 𝐵 ) → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
40 22 39 jaoi ⊢ ( ( 𝑋 = 𝐴 ∨ 𝑋 = 𝐵 ) → ( ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) → ( ( 𝑍 = 𝐴 ∨ 𝑍 = 𝐵 ) → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) ) ) )
41 40 3imp ⊢ ( ( ( 𝑋 = 𝐴 ∨ 𝑋 = 𝐵 ) ∧ ( 𝑌 = 𝐴 ∨ 𝑌 = 𝐵 ) ∧ ( 𝑍 = 𝐴 ∨ 𝑍 = 𝐵 ) ) → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) )
42 1 2 3 41 syl3an ⊢ ( ( 𝑋 ∈ { 𝐴 , 𝐵 } ∧ 𝑌 ∈ { 𝐴 , 𝐵 } ∧ 𝑍 ∈ { 𝐴 , 𝐵 } ) → ( ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) → 𝑌 = 𝑍 ) )
43 42 imp ⊢ ( ( ( 𝑋 ∈ { 𝐴 , 𝐵 } ∧ 𝑌 ∈ { 𝐴 , 𝐵 } ∧ 𝑍 ∈ { 𝐴 , 𝐵 } ) ∧ ( 𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋 ) ) → 𝑌 = 𝑍 )