Theorem altopthsn

Description: Two alternate ordered pairs are equal iff the singletons of their respective elements are equal. Note that this holds regardless of sethood of any of the elements. (Contributed by Scott Fenton, 16-Apr-2012)

	Ref	Expression
Assertion	altopthsn	⊢ ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ( { 𝐴 } = { 𝐶 } ∧ { 𝐵 } = { 𝐷 } ) )

Proof

Step	Hyp	Ref	Expression
1		df-altop	⊢ ⟪ 𝐴 , 𝐵 ⟫ = { { 𝐴 } , { 𝐴 , { 𝐵 } } }
2		df-altop	⊢ ⟪ 𝐶 , 𝐷 ⟫ = { { 𝐶 } , { 𝐶 , { 𝐷 } } }
3	1 2	eqeq12i	⊢ ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } )
4		snex	⊢ { 𝐴 } ∈ V
5		prex	⊢ { 𝐴 , { 𝐵 } } ∈ V
6		snex	⊢ { 𝐶 } ∈ V
7		prex	⊢ { 𝐶 , { 𝐷 } } ∈ V
8	4 5 6 7	preq12b	⊢ ( { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } ↔ ( ( { 𝐴 } = { 𝐶 } ∧ { 𝐴 , { 𝐵 } } = { 𝐶 , { 𝐷 } } ) ∨ ( { 𝐴 } = { 𝐶 , { 𝐷 } } ∧ { 𝐴 , { 𝐵 } } = { 𝐶 } ) ) )
9		simpl	⊢ ( ( { 𝐴 } = { 𝐶 } ∧ { 𝐴 , { 𝐵 } } = { 𝐶 , { 𝐷 } } ) → { 𝐴 } = { 𝐶 } )
10		snsspr1	⊢ { 𝐴 } ⊆ { 𝐴 , { 𝐵 } }
11		sseq2	⊢ ( { 𝐴 , { 𝐵 } } = { 𝐶 } → ( { 𝐴 } ⊆ { 𝐴 , { 𝐵 } } ↔ { 𝐴 } ⊆ { 𝐶 } ) )
12	10 11	mpbii	⊢ ( { 𝐴 , { 𝐵 } } = { 𝐶 } → { 𝐴 } ⊆ { 𝐶 } )
13	12	adantl	⊢ ( ( { 𝐴 } = { 𝐶 , { 𝐷 } } ∧ { 𝐴 , { 𝐵 } } = { 𝐶 } ) → { 𝐴 } ⊆ { 𝐶 } )
14		snsspr1	⊢ { 𝐶 } ⊆ { 𝐶 , { 𝐷 } }
15		sseq2	⊢ ( { 𝐴 } = { 𝐶 , { 𝐷 } } → ( { 𝐶 } ⊆ { 𝐴 } ↔ { 𝐶 } ⊆ { 𝐶 , { 𝐷 } } ) )
16	14 15	mpbiri	⊢ ( { 𝐴 } = { 𝐶 , { 𝐷 } } → { 𝐶 } ⊆ { 𝐴 } )
17	16	adantr	⊢ ( ( { 𝐴 } = { 𝐶 , { 𝐷 } } ∧ { 𝐴 , { 𝐵 } } = { 𝐶 } ) → { 𝐶 } ⊆ { 𝐴 } )
18	13 17	eqssd	⊢ ( ( { 𝐴 } = { 𝐶 , { 𝐷 } } ∧ { 𝐴 , { 𝐵 } } = { 𝐶 } ) → { 𝐴 } = { 𝐶 } )
19	9 18	jaoi	⊢ ( ( ( { 𝐴 } = { 𝐶 } ∧ { 𝐴 , { 𝐵 } } = { 𝐶 , { 𝐷 } } ) ∨ ( { 𝐴 } = { 𝐶 , { 𝐷 } } ∧ { 𝐴 , { 𝐵 } } = { 𝐶 } ) ) → { 𝐴 } = { 𝐶 } )
20	8 19	sylbi	⊢ ( { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } → { 𝐴 } = { 𝐶 } )
21		uneq1	⊢ ( { 𝐴 } = { 𝐶 } → ( { 𝐴 } ∪ { { 𝐵 } } ) = ( { 𝐶 } ∪ { { 𝐵 } } ) )
22		df-pr	⊢ { 𝐴 , { 𝐵 } } = ( { 𝐴 } ∪ { { 𝐵 } } )
23		df-pr	⊢ { 𝐶 , { 𝐵 } } = ( { 𝐶 } ∪ { { 𝐵 } } )
24	21 22 23	3eqtr4g	⊢ ( { 𝐴 } = { 𝐶 } → { 𝐴 , { 𝐵 } } = { 𝐶 , { 𝐵 } } )
25	24	preq2d	⊢ ( { 𝐴 } = { 𝐶 } → { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐴 } , { 𝐶 , { 𝐵 } } } )
26		preq1	⊢ ( { 𝐴 } = { 𝐶 } → { { 𝐴 } , { 𝐶 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐵 } } } )
27	25 26	eqtrd	⊢ ( { 𝐴 } = { 𝐶 } → { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐵 } } } )
28	27	eqeq1d	⊢ ( { 𝐴 } = { 𝐶 } → ( { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } ↔ { { 𝐶 } , { 𝐶 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } ) )
29	28	biimpd	⊢ ( { 𝐴 } = { 𝐶 } → ( { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } → { { 𝐶 } , { 𝐶 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } ) )
30		prex	⊢ { 𝐶 , { 𝐵 } } ∈ V
31	30 7	preqr2	⊢ ( { { 𝐶 } , { 𝐶 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } → { 𝐶 , { 𝐵 } } = { 𝐶 , { 𝐷 } } )
32		snex	⊢ { 𝐵 } ∈ V
33		snex	⊢ { 𝐷 } ∈ V
34	32 33	preqr2	⊢ ( { 𝐶 , { 𝐵 } } = { 𝐶 , { 𝐷 } } → { 𝐵 } = { 𝐷 } )
35	31 34	syl	⊢ ( { { 𝐶 } , { 𝐶 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } → { 𝐵 } = { 𝐷 } )
36	29 35	syl6com	⊢ ( { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } → ( { 𝐴 } = { 𝐶 } → { 𝐵 } = { 𝐷 } ) )
37	20 36	jcai	⊢ ( { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } → ( { 𝐴 } = { 𝐶 } ∧ { 𝐵 } = { 𝐷 } ) )
38		preq2	⊢ ( { 𝐵 } = { 𝐷 } → { 𝐶 , { 𝐵 } } = { 𝐶 , { 𝐷 } } )
39	38	preq2d	⊢ ( { 𝐵 } = { 𝐷 } → { { 𝐶 } , { 𝐶 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } )
40	27 39	sylan9eq	⊢ ( ( { 𝐴 } = { 𝐶 } ∧ { 𝐵 } = { 𝐷 } ) → { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } )
41	37 40	impbii	⊢ ( { { 𝐴 } , { 𝐴 , { 𝐵 } } } = { { 𝐶 } , { 𝐶 , { 𝐷 } } } ↔ ( { 𝐴 } = { 𝐶 } ∧ { 𝐵 } = { 𝐷 } ) )
42	3 41	bitri	⊢ ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ( { 𝐴 } = { 𝐶 } ∧ { 𝐵 } = { 𝐷 } ) )