Theorem en2eqpr

Description: Building a set with two elements. (Contributed by FL, 11-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	en2eqpr	⊢ ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ≠ 𝐵 → 𝐶 = { 𝐴 , 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		2onn	⊢ 2o ∈ ω
2		nnfi	⊢ ( 2o ∈ ω → 2o ∈ Fin )
3	1 2	ax-mp	⊢ 2o ∈ Fin
4		simpl1	⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐶 ≈ 2o )
5		enfii	⊢ ( ( 2o ∈ Fin ∧ 𝐶 ≈ 2o ) → 𝐶 ∈ Fin )
6	3 4 5	sylancr	⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐶 ∈ Fin )
7		simpl2	⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝐶 )
8		simpl3	⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝐶 )
9	7 8	prssd	⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ⊆ 𝐶 )
10		pr2nelem	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
11	10	3expa	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
12	11	3adantl1	⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
13	4	ensymd	⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 2o ≈ 𝐶 )
14		entr	⊢ ( ( { 𝐴 , 𝐵 } ≈ 2o ∧ 2o ≈ 𝐶 ) → { 𝐴 , 𝐵 } ≈ 𝐶 )
15	12 13 14	syl2anc	⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 𝐶 )
16		fisseneq	⊢ ( ( 𝐶 ∈ Fin ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ∧ { 𝐴 , 𝐵 } ≈ 𝐶 ) → { 𝐴 , 𝐵 } = 𝐶 )
17	6 9 15 16	syl3anc	⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } = 𝐶 )
18	17	eqcomd	⊢ ( ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐶 = { 𝐴 , 𝐵 } )
19	18	ex	⊢ ( ( 𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ≠ 𝐵 → 𝐶 = { 𝐴 , 𝐵 } ) )