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 33426
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 33423 . . 3 𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
2 df-altop 33423 . . 3 𝐶, 𝐷⟫ = {{𝐶}, {𝐶, {𝐷}}}
31, 2eqeq12i 2839 . 2 (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4 snex 5335 . . . . . 6 {𝐴} ∈ V
5 prex 5336 . . . . . 6 {𝐴, {𝐵}} ∈ V
6 snex 5335 . . . . . 6 {𝐶} ∈ V
7 prex 5336 . . . . . 6 {𝐶, {𝐷}} ∈ V
84, 5, 6, 7preq12b 4784 . . . . 5 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})))
9 simpl 485 . . . . . 6 (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) → {𝐴} = {𝐶})
10 snsspr1 4750 . . . . . . . . 9 {𝐴} ⊆ {𝐴, {𝐵}}
11 sseq2 3996 . . . . . . . . 9 ({𝐴, {𝐵}} = {𝐶} → ({𝐴} ⊆ {𝐴, {𝐵}} ↔ {𝐴} ⊆ {𝐶}))
1210, 11mpbii 235 . . . . . . . 8 ({𝐴, {𝐵}} = {𝐶} → {𝐴} ⊆ {𝐶})
1312adantl 484 . . . . . . 7 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} ⊆ {𝐶})
14 snsspr1 4750 . . . . . . . . 9 {𝐶} ⊆ {𝐶, {𝐷}}
15 sseq2 3996 . . . . . . . . 9 ({𝐴} = {𝐶, {𝐷}} → ({𝐶} ⊆ {𝐴} ↔ {𝐶} ⊆ {𝐶, {𝐷}}))
1614, 15mpbiri 260 . . . . . . . 8 ({𝐴} = {𝐶, {𝐷}} → {𝐶} ⊆ {𝐴})
1716adantr 483 . . . . . . 7 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐶} ⊆ {𝐴})
1813, 17eqssd 3987 . . . . . 6 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} = {𝐶})
199, 18jaoi 853 . . . . 5 ((({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})) → {𝐴} = {𝐶})
208, 19sylbi 219 . . . 4 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐴} = {𝐶})
21 uneq1 4135 . . . . . . . . . 10 ({𝐴} = {𝐶} → ({𝐴} ∪ {{𝐵}}) = ({𝐶} ∪ {{𝐵}}))
22 df-pr 4573 . . . . . . . . . 10 {𝐴, {𝐵}} = ({𝐴} ∪ {{𝐵}})
23 df-pr 4573 . . . . . . . . . 10 {𝐶, {𝐵}} = ({𝐶} ∪ {{𝐵}})
2421, 22, 233eqtr4g 2884 . . . . . . . . 9 ({𝐴} = {𝐶} → {𝐴, {𝐵}} = {𝐶, {𝐵}})
2524preq2d 4679 . . . . . . . 8 ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐴}, {𝐶, {𝐵}}})
26 preq1 4672 . . . . . . . 8 ({𝐴} = {𝐶} → {{𝐴}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
2725, 26eqtrd 2859 . . . . . . 7 ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
2827eqeq1d 2826 . . . . . 6 ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
2928biimpd 231 . . . . 5 ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
30 prex 5336 . . . . . . 7 {𝐶, {𝐵}} ∈ V
3130, 7preqr2 4783 . . . . . 6 ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
32 snex 5335 . . . . . . 7 {𝐵} ∈ V
33 snex 5335 . . . . . . 7 {𝐷} ∈ V
3432, 33preqr2 4783 . . . . . 6 ({𝐶, {𝐵}} = {𝐶, {𝐷}} → {𝐵} = {𝐷})
3531, 34syl 17 . . . . 5 ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐵} = {𝐷})
3629, 35syl6com 37 . . . 4 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} → {𝐵} = {𝐷}))
3720, 36jcai 519 . . 3 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
38 preq2 4673 . . . . 5 ({𝐵} = {𝐷} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
3938preq2d 4679 . . . 4 ({𝐵} = {𝐷} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4027, 39sylan9eq 2879 . . 3 (({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}) → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4137, 40impbii 211 . 2 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
423, 41bitri 277 1 (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  wo 843   = wceq 1536  cun 3937  wss 3939  {csn 4570  {cpr 4572  caltop 33421
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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-sn 4571  df-pr 4573  df-altop 33423
This theorem is referenced by:  altopeq12  33427  altopth1  33430  altopth2  33431  altopthg  33432  altopthbg  33433
  Copyright terms: Public domain W3C validator