Theorem altopthsn 36903

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 36900	. . 3 ⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
2		df-altop 36900	. . 3 ⊢ ⟪𝐶, 𝐷⟫ = {{𝐶}, {𝐶, {𝐷}}}
3	1, 2	eqeq12i 2781	. 2 ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4		snex 5401	. . . . . 6 ⊢ {𝐴} ∈ V
5		prex 5400	. . . . . 6 ⊢ {𝐴, {𝐵}} ∈ V
6		snex 5401	. . . . . 6 ⊢ {𝐶} ∈ V
7		prex 5400	. . . . . 6 ⊢ {𝐶, {𝐷}} ∈ V
8	4, 5, 6, 7	preq12b 4808	. . . . 5 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})))
9		simpl 488	. . . . . 6 ⊢ (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) → {𝐴} = {𝐶})
10		snsspr1 4773	. . . . . . . . 9 ⊢ {𝐴} ⊆ {𝐴, {𝐵}}
11		sseq2 3939	. . . . . . . . 9 ⊢ ({𝐴, {𝐵}} = {𝐶} → ({𝐴} ⊆ {𝐴, {𝐵}} ↔ {𝐴} ⊆ {𝐶}))
12	10, 11	mpbii 236	. . . . . . . 8 ⊢ ({𝐴, {𝐵}} = {𝐶} → {𝐴} ⊆ {𝐶})
13	12	adantl 487	. . . . . . 7 ⊢ (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} ⊆ {𝐶})
14		snsspr1 4773	. . . . . . . . 9 ⊢ {𝐶} ⊆ {𝐶, {𝐷}}
15		sseq2 3939	. . . . . . . . 9 ⊢ ({𝐴} = {𝐶, {𝐷}} → ({𝐶} ⊆ {𝐴} ↔ {𝐶} ⊆ {𝐶, {𝐷}}))
16	14, 15	mpbiri 261	. . . . . . . 8 ⊢ ({𝐴} = {𝐶, {𝐷}} → {𝐶} ⊆ {𝐴})
17	16	adantr 486	. . . . . . 7 ⊢ (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐶} ⊆ {𝐴})
18	13, 17	eqssd 3930	. . . . . 6 ⊢ (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} = {𝐶})
19	9, 18	jaoi 871	. . . . 5 ⊢ ((({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})) → {𝐴} = {𝐶})
20	8, 19	sylbi 220	. . . 4 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐴} = {𝐶})
21		uneq1 4163	. . . . . . . . . 10 ⊢ ({𝐴} = {𝐶} → ({𝐴} ∪ {{𝐵}}) = ({𝐶} ∪ {{𝐵}}))
22		df-pr 4591	. . . . . . . . . 10 ⊢ {𝐴, {𝐵}} = ({𝐴} ∪ {{𝐵}})
23		df-pr 4591	. . . . . . . . . 10 ⊢ {𝐶, {𝐵}} = ({𝐶} ∪ {{𝐵}})
24	21, 22, 23	3eqtr4g 2823	. . . . . . . . 9 ⊢ ({𝐴} = {𝐶} → {𝐴, {𝐵}} = {𝐶, {𝐵}})
25	24	preq2d 4701	. . . . . . . 8 ⊢ ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐴}, {𝐶, {𝐵}}})
26		preq1 4694	. . . . . . . 8 ⊢ ({𝐴} = {𝐶} → {{𝐴}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
27	25, 26	eqtrd 2798	. . . . . . 7 ⊢ ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
28	27	eqeq1d 2765	. . . . . 6 ⊢ ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
29	28	biimpd 232	. . . . 5 ⊢ ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
30		prex 5400	. . . . . . 7 ⊢ {𝐶, {𝐵}} ∈ V
31	30, 7	preqr2 4807	. . . . . 6 ⊢ ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
32		snex 5401	. . . . . . 7 ⊢ {𝐵} ∈ V
33		snex 5401	. . . . . . 7 ⊢ {𝐷} ∈ V
34	32, 33	preqr2 4807	. . . . . 6 ⊢ ({𝐶, {𝐵}} = {𝐶, {𝐷}} → {𝐵} = {𝐷})
35	31, 34	syl 18	. . . . 5 ⊢ ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐵} = {𝐷})
36	29, 35	syl6com 38	. . . 4 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} → {𝐵} = {𝐷}))
37	20, 36	jcai 526	. . 3 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
38		preq2 4695	. . . . 5 ⊢ ({𝐵} = {𝐷} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
39	38	preq2d 4701	. . . 4 ⊢ ({𝐵} = {𝐷} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
40	27, 39	sylan9eq 2818	. . 3 ⊢ (({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}) → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
41	37, 40	impbii 212	. 2 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
42	3, 41	bitri 278	1 ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ⊆ wss 3900   ∪ cun 4152  {csn 4588  {cpr 4590  ⟪caltop 36898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591  df-altop 36900

This theorem is used by:  altopeq12  36904  altopth1  36907  altopth2  36908  altopthg  36909  altopthbg  36910