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 32394
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 32391 . . 3 𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
2 df-altop 32391 . . 3 𝐶, 𝐷⟫ = {{𝐶}, {𝐶, {𝐷}}}
31, 2eqeq12i 2827 . 2 (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4 snex 5105 . . . . . 6 {𝐴} ∈ V
5 prex 5106 . . . . . 6 {𝐴, {𝐵}} ∈ V
6 snex 5105 . . . . . 6 {𝐶} ∈ V
7 prex 5106 . . . . . 6 {𝐶, {𝐷}} ∈ V
84, 5, 6, 7preq12b 4576 . . . . 5 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})))
9 simpl 470 . . . . . 6 (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) → {𝐴} = {𝐶})
10 snsspr1 4542 . . . . . . . . 9 {𝐴} ⊆ {𝐴, {𝐵}}
11 sseq2 3831 . . . . . . . . 9 ({𝐴, {𝐵}} = {𝐶} → ({𝐴} ⊆ {𝐴, {𝐵}} ↔ {𝐴} ⊆ {𝐶}))
1210, 11mpbii 224 . . . . . . . 8 ({𝐴, {𝐵}} = {𝐶} → {𝐴} ⊆ {𝐶})
1312adantl 469 . . . . . . 7 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} ⊆ {𝐶})
14 snsspr1 4542 . . . . . . . . 9 {𝐶} ⊆ {𝐶, {𝐷}}
15 sseq2 3831 . . . . . . . . 9 ({𝐴} = {𝐶, {𝐷}} → ({𝐶} ⊆ {𝐴} ↔ {𝐶} ⊆ {𝐶, {𝐷}}))
1614, 15mpbiri 249 . . . . . . . 8 ({𝐴} = {𝐶, {𝐷}} → {𝐶} ⊆ {𝐴})
1716adantr 468 . . . . . . 7 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐶} ⊆ {𝐴})
1813, 17eqssd 3822 . . . . . 6 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} = {𝐶})
199, 18jaoi 875 . . . . 5 ((({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})) → {𝐴} = {𝐶})
208, 19sylbi 208 . . . 4 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐴} = {𝐶})
21 uneq1 3966 . . . . . . . . . 10 ({𝐴} = {𝐶} → ({𝐴} ∪ {{𝐵}}) = ({𝐶} ∪ {{𝐵}}))
22 df-pr 4380 . . . . . . . . . 10 {𝐴, {𝐵}} = ({𝐴} ∪ {{𝐵}})
23 df-pr 4380 . . . . . . . . . 10 {𝐶, {𝐵}} = ({𝐶} ∪ {{𝐵}})
2421, 22, 233eqtr4g 2872 . . . . . . . . 9 ({𝐴} = {𝐶} → {𝐴, {𝐵}} = {𝐶, {𝐵}})
2524preq2d 4473 . . . . . . . 8 ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐴}, {𝐶, {𝐵}}})
26 preq1 4466 . . . . . . . 8 ({𝐴} = {𝐶} → {{𝐴}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
2725, 26eqtrd 2847 . . . . . . 7 ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
2827eqeq1d 2815 . . . . . 6 ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
2928biimpd 220 . . . . 5 ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
30 prex 5106 . . . . . . 7 {𝐶, {𝐵}} ∈ V
3130, 7preqr2 4575 . . . . . 6 ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
32 snex 5105 . . . . . . 7 {𝐵} ∈ V
33 snex 5105 . . . . . . 7 {𝐷} ∈ V
3432, 33preqr2 4575 . . . . . 6 ({𝐶, {𝐵}} = {𝐶, {𝐷}} → {𝐵} = {𝐷})
3531, 34syl 17 . . . . 5 ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐵} = {𝐷})
3629, 35syl6com 37 . . . 4 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} → {𝐵} = {𝐷}))
3720, 36jcai 508 . . 3 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
38 preq2 4467 . . . . 5 ({𝐵} = {𝐷} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
3938preq2d 4473 . . . 4 ({𝐵} = {𝐷} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4027, 39sylan9eq 2867 . . 3 (({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}) → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4137, 40impbii 200 . 2 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
423, 41bitri 266 1 (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wo 865   = wceq 1637  cun 3774  wss 3776  {csn 4377  {cpr 4379  caltop 32389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pr 5103
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-sn 4378  df-pr 4380  df-altop 32391
This theorem is referenced by:  altopeq12  32395  altopth1  32398  altopth2  32399  altopthg  32400  altopthbg  32401
  Copyright terms: Public domain W3C validator