Theorem altopthsn 35942

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 35939	. . 3 ⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
2		df-altop 35939	. . 3 ⊢ ⟪𝐶, 𝐷⟫ = {{𝐶}, {𝐶, {𝐷}}}
3	1, 2	eqeq12i 2747	. 2 ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4		snex 5386	. . . . . 6 ⊢ {𝐴} ∈ V
5		prex 5387	. . . . . 6 ⊢ {𝐴, {𝐵}} ∈ V
6		snex 5386	. . . . . 6 ⊢ {𝐶} ∈ V
7		prex 5387	. . . . . 6 ⊢ {𝐶, {𝐷}} ∈ V
8	4, 5, 6, 7	preq12b 4810	. . . . 5 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})))
9		simpl 482	. . . . . 6 ⊢ (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) → {𝐴} = {𝐶})
10		snsspr1 4774	. . . . . . . . 9 ⊢ {𝐴} ⊆ {𝐴, {𝐵}}
11		sseq2 3970	. . . . . . . . 9 ⊢ ({𝐴, {𝐵}} = {𝐶} → ({𝐴} ⊆ {𝐴, {𝐵}} ↔ {𝐴} ⊆ {𝐶}))
12	10, 11	mpbii 233	. . . . . . . 8 ⊢ ({𝐴, {𝐵}} = {𝐶} → {𝐴} ⊆ {𝐶})
13	12	adantl 481	. . . . . . 7 ⊢ (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} ⊆ {𝐶})
14		snsspr1 4774	. . . . . . . . 9 ⊢ {𝐶} ⊆ {𝐶, {𝐷}}
15		sseq2 3970	. . . . . . . . 9 ⊢ ({𝐴} = {𝐶, {𝐷}} → ({𝐶} ⊆ {𝐴} ↔ {𝐶} ⊆ {𝐶, {𝐷}}))
16	14, 15	mpbiri 258	. . . . . . . 8 ⊢ ({𝐴} = {𝐶, {𝐷}} → {𝐶} ⊆ {𝐴})
17	16	adantr 480	. . . . . . 7 ⊢ (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐶} ⊆ {𝐴})
18	13, 17	eqssd 3961	. . . . . 6 ⊢ (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} = {𝐶})
19	9, 18	jaoi 857	. . . . 5 ⊢ ((({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})) → {𝐴} = {𝐶})
20	8, 19	sylbi 217	. . . 4 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐴} = {𝐶})
21		uneq1 4120	. . . . . . . . . 10 ⊢ ({𝐴} = {𝐶} → ({𝐴} ∪ {{𝐵}}) = ({𝐶} ∪ {{𝐵}}))
22		df-pr 4588	. . . . . . . . . 10 ⊢ {𝐴, {𝐵}} = ({𝐴} ∪ {{𝐵}})
23		df-pr 4588	. . . . . . . . . 10 ⊢ {𝐶, {𝐵}} = ({𝐶} ∪ {{𝐵}})
24	21, 22, 23	3eqtr4g 2789	. . . . . . . . 9 ⊢ ({𝐴} = {𝐶} → {𝐴, {𝐵}} = {𝐶, {𝐵}})
25	24	preq2d 4700	. . . . . . . 8 ⊢ ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐴}, {𝐶, {𝐵}}})
26		preq1 4693	. . . . . . . 8 ⊢ ({𝐴} = {𝐶} → {{𝐴}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
27	25, 26	eqtrd 2764	. . . . . . 7 ⊢ ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
28	27	eqeq1d 2731	. . . . . 6 ⊢ ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
29	28	biimpd 229	. . . . 5 ⊢ ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
30		prex 5387	. . . . . . 7 ⊢ {𝐶, {𝐵}} ∈ V
31	30, 7	preqr2 4809	. . . . . 6 ⊢ ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
32		snex 5386	. . . . . . 7 ⊢ {𝐵} ∈ V
33		snex 5386	. . . . . . 7 ⊢ {𝐷} ∈ V
34	32, 33	preqr2 4809	. . . . . 6 ⊢ ({𝐶, {𝐵}} = {𝐶, {𝐷}} → {𝐵} = {𝐷})
35	31, 34	syl 17	. . . . 5 ⊢ ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐵} = {𝐷})
36	29, 35	syl6com 37	. . . 4 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} → {𝐵} = {𝐷}))
37	20, 36	jcai 516	. . 3 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
38		preq2 4694	. . . . 5 ⊢ ({𝐵} = {𝐷} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
39	38	preq2d 4700	. . . 4 ⊢ ({𝐵} = {𝐷} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
40	27, 39	sylan9eq 2784	. . 3 ⊢ (({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}) → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
41	37, 40	impbii 209	. 2 ⊢ ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
42	3, 41	bitri 275	1 ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∪ cun 3909   ⊆ wss 3911  {csn 4585  {cpr 4587  ⟪caltop 35937

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-sn 4586  df-pr 4588  df-altop 35939

This theorem is referenced by:  altopeq12  35943  altopth1  35946  altopth2  35947  altopthg  35948  altopthbg  35949