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	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ) ↔ { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		3ianor	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ) ↔ ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) )
2		df-3or	⊢ ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) ↔ ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ) ∨ ¬ 𝐶 ≠ 𝐵 ) )
3	1 2	bitri	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ) ↔ ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ) ∨ ¬ 𝐶 ≠ 𝐵 ) )
4		orass	⊢ ( ( ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ) ∨ ¬ 𝐶 ≠ 𝐵 ) ∨ ¬ 𝐶 ∈ V ) ↔ ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ) ∨ ( ¬ 𝐶 ≠ 𝐵 ∨ ¬ 𝐶 ∈ V ) ) )
5		ianor	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ↔ ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ) )
6		tpprceq3	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) → { 𝐵 , 𝐴 , 𝐶 } = { 𝐵 , 𝐴 } )
7	5 6	sylbir	⊢ ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ) → { 𝐵 , 𝐴 , 𝐶 } = { 𝐵 , 𝐴 } )
8		tpcoma	⊢ { 𝐵 , 𝐴 , 𝐶 } = { 𝐴 , 𝐵 , 𝐶 }
9		prcom	⊢ { 𝐵 , 𝐴 } = { 𝐴 , 𝐵 }
10	7 8 9	3eqtr3g	⊢ ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
11		orcom	⊢ ( ( ¬ 𝐶 ≠ 𝐵 ∨ ¬ 𝐶 ∈ V ) ↔ ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐵 ) )
12		ianor	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐵 ) ↔ ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐵 ) )
13	11 12	bitr4i	⊢ ( ( ¬ 𝐶 ≠ 𝐵 ∨ ¬ 𝐶 ∈ V ) ↔ ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐵 ) )
14		tpprceq3	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐵 ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
15	13 14	sylbi	⊢ ( ( ¬ 𝐶 ≠ 𝐵 ∨ ¬ 𝐶 ∈ V ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
16	10 15	jaoi	⊢ ( ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ) ∨ ( ¬ 𝐶 ≠ 𝐵 ∨ ¬ 𝐶 ∈ V ) ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
17	4 16	sylbi	⊢ ( ( ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ) ∨ ¬ 𝐶 ≠ 𝐵 ) ∨ ¬ 𝐶 ∈ V ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
18	17	orcs	⊢ ( ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ) ∨ ¬ 𝐶 ≠ 𝐵 ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
19	3 18	sylbi	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
20		df-tp	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
21	20	eqeq1i	⊢ ( { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } ↔ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) = { 𝐴 , 𝐵 } )
22		ssequn2	⊢ ( { 𝐶 } ⊆ { 𝐴 , 𝐵 } ↔ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) = { 𝐴 , 𝐵 } )
23		snssg	⊢ ( 𝐶 ∈ V → ( 𝐶 ∈ { 𝐴 , 𝐵 } ↔ { 𝐶 } ⊆ { 𝐴 , 𝐵 } ) )
24		elpri	⊢ ( 𝐶 ∈ { 𝐴 , 𝐵 } → ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) )
25		nne	⊢ ( ¬ 𝐶 ≠ 𝐴 ↔ 𝐶 = 𝐴 )
26		3mix2	⊢ ( ¬ 𝐶 ≠ 𝐴 → ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) )
27	25 26	sylbir	⊢ ( 𝐶 = 𝐴 → ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) )
28		nne	⊢ ( ¬ 𝐶 ≠ 𝐵 ↔ 𝐶 = 𝐵 )
29		3mix3	⊢ ( ¬ 𝐶 ≠ 𝐵 → ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) )
30	28 29	sylbir	⊢ ( 𝐶 = 𝐵 → ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) )
31	27 30	jaoi	⊢ ( ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) → ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) )
32	24 31	syl	⊢ ( 𝐶 ∈ { 𝐴 , 𝐵 } → ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) )
33	23 32	biimtrrdi	⊢ ( 𝐶 ∈ V → ( { 𝐶 } ⊆ { 𝐴 , 𝐵 } → ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) ) )
34		3mix1	⊢ ( ¬ 𝐶 ∈ V → ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) )
35	34	a1d	⊢ ( ¬ 𝐶 ∈ V → ( { 𝐶 } ⊆ { 𝐴 , 𝐵 } → ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) ) )
36	33 35	pm2.61i	⊢ ( { 𝐶 } ⊆ { 𝐴 , 𝐵 } → ( ¬ 𝐶 ∈ V ∨ ¬ 𝐶 ≠ 𝐴 ∨ ¬ 𝐶 ≠ 𝐵 ) )
37	36 1	sylibr	⊢ ( { 𝐶 } ⊆ { 𝐴 , 𝐵 } → ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ) )
38	22 37	sylbir	⊢ ( ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) = { 𝐴 , 𝐵 } → ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ) )
39	21 38	sylbi	⊢ ( { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } → ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ) )
40	19 39	impbii	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ∧ 𝐶 ≠ 𝐵 ) ↔ { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )

Metamath Proof Explorer

Theorem tppreqb

Proof