Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  altopthsn Structured version   Visualization version   GIF version

Theorem altopthsn 32193
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
StepHypRef Expression
1 df-altop 32190 . . 3 𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
2 df-altop 32190 . . 3 𝐶, 𝐷⟫ = {{𝐶}, {𝐶, {𝐷}}}
31, 2eqeq12i 2665 . 2 (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4 snex 4938 . . . . . 6 {𝐴} ∈ V
5 prex 4939 . . . . . 6 {𝐴, {𝐵}} ∈ V
6 snex 4938 . . . . . 6 {𝐶} ∈ V
7 prex 4939 . . . . . 6 {𝐶, {𝐷}} ∈ V
84, 5, 6, 7preq12b 4413 . . . . 5 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})))
9 simpl 472 . . . . . 6 (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) → {𝐴} = {𝐶})
10 snsspr1 4377 . . . . . . . . 9 {𝐴} ⊆ {𝐴, {𝐵}}
11 sseq2 3660 . . . . . . . . 9 ({𝐴, {𝐵}} = {𝐶} → ({𝐴} ⊆ {𝐴, {𝐵}} ↔ {𝐴} ⊆ {𝐶}))
1210, 11mpbii 223 . . . . . . . 8 ({𝐴, {𝐵}} = {𝐶} → {𝐴} ⊆ {𝐶})
1312adantl 481 . . . . . . 7 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} ⊆ {𝐶})
14 snsspr1 4377 . . . . . . . . 9 {𝐶} ⊆ {𝐶, {𝐷}}
15 sseq2 3660 . . . . . . . . 9 ({𝐴} = {𝐶, {𝐷}} → ({𝐶} ⊆ {𝐴} ↔ {𝐶} ⊆ {𝐶, {𝐷}}))
1614, 15mpbiri 248 . . . . . . . 8 ({𝐴} = {𝐶, {𝐷}} → {𝐶} ⊆ {𝐴})
1716adantr 480 . . . . . . 7 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐶} ⊆ {𝐴})
1813, 17eqssd 3653 . . . . . 6 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} = {𝐶})
199, 18jaoi 393 . . . . 5 ((({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})) → {𝐴} = {𝐶})
208, 19sylbi 207 . . . 4 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐴} = {𝐶})
21 uneq1 3793 . . . . . . . . . 10 ({𝐴} = {𝐶} → ({𝐴} ∪ {{𝐵}}) = ({𝐶} ∪ {{𝐵}}))
22 df-pr 4213 . . . . . . . . . 10 {𝐴, {𝐵}} = ({𝐴} ∪ {{𝐵}})
23 df-pr 4213 . . . . . . . . . 10 {𝐶, {𝐵}} = ({𝐶} ∪ {{𝐵}})
2421, 22, 233eqtr4g 2710 . . . . . . . . 9 ({𝐴} = {𝐶} → {𝐴, {𝐵}} = {𝐶, {𝐵}})
2524preq2d 4307 . . . . . . . 8 ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐴}, {𝐶, {𝐵}}})
26 preq1 4300 . . . . . . . 8 ({𝐴} = {𝐶} → {{𝐴}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
2725, 26eqtrd 2685 . . . . . . 7 ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
2827eqeq1d 2653 . . . . . 6 ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
2928biimpd 219 . . . . 5 ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
30 prex 4939 . . . . . . 7 {𝐶, {𝐵}} ∈ V
3130, 7preqr2 4412 . . . . . 6 ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
32 snex 4938 . . . . . . 7 {𝐵} ∈ V
33 snex 4938 . . . . . . 7 {𝐷} ∈ V
3432, 33preqr2 4412 . . . . . 6 ({𝐶, {𝐵}} = {𝐶, {𝐷}} → {𝐵} = {𝐷})
3531, 34syl 17 . . . . 5 ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐵} = {𝐷})
3629, 35syl6com 37 . . . 4 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} → {𝐵} = {𝐷}))
3720, 36jcai 558 . . 3 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
38 preq2 4301 . . . . 5 ({𝐵} = {𝐷} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
3938preq2d 4307 . . . 4 ({𝐵} = {𝐷} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4027, 39sylan9eq 2705 . . 3 (({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}) → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4137, 40impbii 199 . 2 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
423, 41bitri 264 1 (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 382  wa 383   = wceq 1523  cun 3605  wss 3607  {csn 4210  {cpr 4212  caltop 32188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-sn 4211  df-pr 4213  df-altop 32190
This theorem is referenced by:  altopeq12  32194  altopth1  32197  altopth2  32198  altopthg  32199  altopthbg  32200
  Copyright terms: Public domain W3C validator