Theorem altopthsn 35956

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.)

Assertion

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

Proof of Theorem altopthsn

Step	Hyp	Ref	Expression
1		df-altop 35953	. . 3 ⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
2		df-altop 35953	. . 3 ⊢ ⟪𝐶, 𝐷⟫ = {{𝐶}, {𝐶, {𝐷}}}
3	1, 2	eqeq12i 2748	. 2 ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4		snex 5394	. . . . . 6 ⊢ {𝐴} ∈ V
5		prex 5395	. . . . . 6 ⊢ {𝐴, {𝐵}} ∈ V
6		snex 5394	. . . . . 6 ⊢ {𝐶} ∈ V
7		prex 5395	. . . . . 6 ⊢ {𝐶, {𝐷}} ∈ V
8	4, 5, 6, 7	preq12b 4817	. . . . 5 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})))
9		simpl 482	. . . . . 6 ⊢ (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) → {𝐴} = {𝐶})
10		snsspr1 4781	. . . . . . . . 9 ⊢ {𝐴} ⊆ {𝐴, {𝐵}}
11		sseq2 3976	. . . . . . . . 9 ⊢ ({𝐴, {𝐵}} = {𝐶} → ({𝐴} ⊆ {𝐴, {𝐵}} ↔ {𝐴} ⊆ {𝐶}))
12	10, 11	mpbii 233	. . . . . . . 8 ⊢ ({𝐴, {𝐵}} = {𝐶} → {𝐴} ⊆ {𝐶})
13	12	adantl 481	. . . . . . 7 ⊢ (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} ⊆ {𝐶})
14		snsspr1 4781	. . . . . . . . 9 ⊢ {𝐶} ⊆ {𝐶, {𝐷}}
15		sseq2 3976	. . . . . . . . 9 ⊢ ({𝐴} = {𝐶, {𝐷}} → ({𝐶} ⊆ {𝐴} ↔ {𝐶} ⊆ {𝐶, {𝐷}}))
16	14, 15	mpbiri 258	. . . . . . . 8 ⊢ ({𝐴} = {𝐶, {𝐷}} → {𝐶} ⊆ {𝐴})
17	16	adantr 480	. . . . . . 7 ⊢ (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐶} ⊆ {𝐴})
18	13, 17	eqssd 3967	. . . . . 6 ⊢ (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} = {𝐶})
19	9, 18	jaoi 857	. . . . 5 ⊢ ((({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})) → {𝐴} = {𝐶})
20	8, 19	sylbi 217	. . . 4 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐴} = {𝐶})
21		uneq1 4127	. . . . . . . . . 10 ⊢ ({𝐴} = {𝐶} → ({𝐴} ∪ {{𝐵}}) = ({𝐶} ∪ {{𝐵}}))
22		df-pr 4595	. . . . . . . . . 10 ⊢ {𝐴, {𝐵}} = ({𝐴} ∪ {{𝐵}})
23		df-pr 4595	. . . . . . . . . 10 ⊢ {𝐶, {𝐵}} = ({𝐶} ∪ {{𝐵}})
24	21, 22, 23	3eqtr4g 2790	. . . . . . . . 9 ⊢ ({𝐴} = {𝐶} → {𝐴, {𝐵}} = {𝐶, {𝐵}})
25	24	preq2d 4707	. . . . . . . 8 ⊢ ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐴}, {𝐶, {𝐵}}})
26		preq1 4700	. . . . . . . 8 ⊢ ({𝐴} = {𝐶} → {{𝐴}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
27	25, 26	eqtrd 2765	. . . . . . 7 ⊢ ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
28	27	eqeq1d 2732	. . . . . 6 ⊢ ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
29	28	biimpd 229	. . . . 5 ⊢ ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
30		prex 5395	. . . . . . 7 ⊢ {𝐶, {𝐵}} ∈ V
31	30, 7	preqr2 4816	. . . . . 6 ⊢ ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
32		snex 5394	. . . . . . 7 ⊢ {𝐵} ∈ V
33		snex 5394	. . . . . . 7 ⊢ {𝐷} ∈ V
34	32, 33	preqr2 4816	. . . . . 6 ⊢ ({𝐶, {𝐵}} = {𝐶, {𝐷}} → {𝐵} = {𝐷})
35	31, 34	syl 17	. . . . 5 ⊢ ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐵} = {𝐷})
36	29, 35	syl6com 37	. . . 4 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} → {𝐵} = {𝐷}))
37	20, 36	jcai 516	. . 3 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
38		preq2 4701	. . . . 5 ⊢ ({𝐵} = {𝐷} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
39	38	preq2d 4707	. . . 4 ⊢ ({𝐵} = {𝐷} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
40	27, 39	sylan9eq 2785	. . 3 ⊢ (({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}) → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
41	37, 40	impbii 209	. 2 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
42	3, 41	bitri 275	1 ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∪ cun 3915   ⊆ wss 3917  {csn 4592  {cpr 4594  ⟪caltop 35951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-altop 35953

This theorem is referenced by:  altopeq12  35957  altopth1  35960  altopth2  35961  altopthg  35962  altopthbg  35963