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

Metamath Proof Explorer

Theorem tppreqb

Description: An unordered triple is an unordered pair if and only if one of its elements is a proper class or is identical with one of the another elements. (Contributed by Alexander van der Vekens, 15-Jan-2018)

Ref Expression
Assertion tppreqb 
|- ( -. ( C e. _V /\ C =/= A /\ C =/= B ) <-> { A , B , C } = { A , B } )

Proof

Step Hyp Ref Expression
1 3ianor 
 |-  ( -. ( C e. _V /\ C =/= A /\ C =/= B ) <-> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) )
2 df-3or 
 |-  ( ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) <-> ( ( -. C e. _V \/ -. C =/= A ) \/ -. C =/= B ) )
3 1 2 bitri 
 |-  ( -. ( C e. _V /\ C =/= A /\ C =/= B ) <-> ( ( -. C e. _V \/ -. C =/= A ) \/ -. C =/= B ) )
4 orass 
 |-  ( ( ( ( -. C e. _V \/ -. C =/= A ) \/ -. C =/= B ) \/ -. C e. _V ) <-> ( ( -. C e. _V \/ -. C =/= A ) \/ ( -. C =/= B \/ -. C e. _V ) ) )
5 ianor 
 |-  ( -. ( C e. _V /\ C =/= A ) <-> ( -. C e. _V \/ -. C =/= A ) )
6 tpprceq3 
 |-  ( -. ( C e. _V /\ C =/= A ) -> { B , A , C } = { B , A } )
7 5 6 sylbir 
 |-  ( ( -. C e. _V \/ -. C =/= A ) -> { B , A , C } = { B , A } )
8 tpcoma 
 |-  { B , A , C } = { A , B , C }
9 prcom 
 |-  { B , A } = { A , B }
10 7 8 9 3eqtr3g 
 |-  ( ( -. C e. _V \/ -. C =/= A ) -> { A , B , C } = { A , B } )
11 orcom 
 |-  ( ( -. C =/= B \/ -. C e. _V ) <-> ( -. C e. _V \/ -. C =/= B ) )
12 ianor 
 |-  ( -. ( C e. _V /\ C =/= B ) <-> ( -. C e. _V \/ -. C =/= B ) )
13 11 12 bitr4i 
 |-  ( ( -. C =/= B \/ -. C e. _V ) <-> -. ( C e. _V /\ C =/= B ) )
14 tpprceq3 
 |-  ( -. ( C e. _V /\ C =/= B ) -> { A , B , C } = { A , B } )
15 13 14 sylbi 
 |-  ( ( -. C =/= B \/ -. C e. _V ) -> { A , B , C } = { A , B } )
16 10 15 jaoi 
 |-  ( ( ( -. C e. _V \/ -. C =/= A ) \/ ( -. C =/= B \/ -. C e. _V ) ) -> { A , B , C } = { A , B } )
17 4 16 sylbi 
 |-  ( ( ( ( -. C e. _V \/ -. C =/= A ) \/ -. C =/= B ) \/ -. C e. _V ) -> { A , B , C } = { A , B } )
18 17 orcs 
 |-  ( ( ( -. C e. _V \/ -. C =/= A ) \/ -. C =/= B ) -> { A , B , C } = { A , B } )
19 3 18 sylbi 
 |-  ( -. ( C e. _V /\ C =/= A /\ C =/= B ) -> { A , B , C } = { A , B } )
20 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
21 20 eqeq1i 
 |-  ( { A , B , C } = { A , B } <-> ( { A , B } u. { C } ) = { A , B } )
22 ssequn2 
 |-  ( { C } C_ { A , B } <-> ( { A , B } u. { C } ) = { A , B } )
23 snssg 
 |-  ( C e. _V -> ( C e. { A , B } <-> { C } C_ { A , B } ) )
24 elpri 
 |-  ( C e. { A , B } -> ( C = A \/ C = B ) )
25 nne 
 |-  ( -. C =/= A <-> C = A )
26 3mix2 
 |-  ( -. C =/= A -> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) )
27 25 26 sylbir 
 |-  ( C = A -> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) )
28 nne 
 |-  ( -. C =/= B <-> C = B )
29 3mix3 
 |-  ( -. C =/= B -> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) )
30 28 29 sylbir 
 |-  ( C = B -> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) )
31 27 30 jaoi 
 |-  ( ( C = A \/ C = B ) -> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) )
32 24 31 syl 
 |-  ( C e. { A , B } -> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) )
33 23 32 biimtrrdi 
 |-  ( C e. _V -> ( { C } C_ { A , B } -> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) ) )
34 3mix1 
 |-  ( -. C e. _V -> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) )
35 34 a1d 
 |-  ( -. C e. _V -> ( { C } C_ { A , B } -> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) ) )
36 33 35 pm2.61i 
 |-  ( { C } C_ { A , B } -> ( -. C e. _V \/ -. C =/= A \/ -. C =/= B ) )
37 36 1 sylibr 
 |-  ( { C } C_ { A , B } -> -. ( C e. _V /\ C =/= A /\ C =/= B ) )
38 22 37 sylbir 
 |-  ( ( { A , B } u. { C } ) = { A , B } -> -. ( C e. _V /\ C =/= A /\ C =/= B ) )
39 21 38 sylbi 
 |-  ( { A , B , C } = { A , B } -> -. ( C e. _V /\ C =/= A /\ C =/= B ) )
40 19 39 impbii 
 |-  ( -. ( C e. _V /\ C =/= A /\ C =/= B ) <-> { A , B , C } = { A , B } )