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 34592
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 34589 . . 3 𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
2 df-altop 34589 . . 3 𝐶, 𝐷⟫ = {{𝐶}, {𝐶, {𝐷}}}
31, 2eqeq12i 2751 . 2 (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4 snex 5389 . . . . . 6 {𝐴} ∈ V
5 prex 5390 . . . . . 6 {𝐴, {𝐵}} ∈ V
6 snex 5389 . . . . . 6 {𝐶} ∈ V
7 prex 5390 . . . . . 6 {𝐶, {𝐷}} ∈ V
84, 5, 6, 7preq12b 4809 . . . . 5 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})))
9 simpl 484 . . . . . 6 (({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) → {𝐴} = {𝐶})
10 snsspr1 4775 . . . . . . . . 9 {𝐴} ⊆ {𝐴, {𝐵}}
11 sseq2 3971 . . . . . . . . 9 ({𝐴, {𝐵}} = {𝐶} → ({𝐴} ⊆ {𝐴, {𝐵}} ↔ {𝐴} ⊆ {𝐶}))
1210, 11mpbii 232 . . . . . . . 8 ({𝐴, {𝐵}} = {𝐶} → {𝐴} ⊆ {𝐶})
1312adantl 483 . . . . . . 7 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} ⊆ {𝐶})
14 snsspr1 4775 . . . . . . . . 9 {𝐶} ⊆ {𝐶, {𝐷}}
15 sseq2 3971 . . . . . . . . 9 ({𝐴} = {𝐶, {𝐷}} → ({𝐶} ⊆ {𝐴} ↔ {𝐶} ⊆ {𝐶, {𝐷}}))
1614, 15mpbiri 258 . . . . . . . 8 ({𝐴} = {𝐶, {𝐷}} → {𝐶} ⊆ {𝐴})
1716adantr 482 . . . . . . 7 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐶} ⊆ {𝐴})
1813, 17eqssd 3962 . . . . . 6 (({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶}) → {𝐴} = {𝐶})
199, 18jaoi 856 . . . . 5 ((({𝐴} = {𝐶} ∧ {𝐴, {𝐵}} = {𝐶, {𝐷}}) ∨ ({𝐴} = {𝐶, {𝐷}} ∧ {𝐴, {𝐵}} = {𝐶})) → {𝐴} = {𝐶})
208, 19sylbi 216 . . . 4 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐴} = {𝐶})
21 uneq1 4117 . . . . . . . . . 10 ({𝐴} = {𝐶} → ({𝐴} ∪ {{𝐵}}) = ({𝐶} ∪ {{𝐵}}))
22 df-pr 4590 . . . . . . . . . 10 {𝐴, {𝐵}} = ({𝐴} ∪ {{𝐵}})
23 df-pr 4590 . . . . . . . . . 10 {𝐶, {𝐵}} = ({𝐶} ∪ {{𝐵}})
2421, 22, 233eqtr4g 2798 . . . . . . . . 9 ({𝐴} = {𝐶} → {𝐴, {𝐵}} = {𝐶, {𝐵}})
2524preq2d 4702 . . . . . . . 8 ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐴}, {𝐶, {𝐵}}})
26 preq1 4695 . . . . . . . 8 ({𝐴} = {𝐶} → {{𝐴}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
2725, 26eqtrd 2773 . . . . . . 7 ({𝐴} = {𝐶} → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐵}}})
2827eqeq1d 2735 . . . . . 6 ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
2928biimpd 228 . . . . 5 ({𝐴} = {𝐶} → ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}}))
30 prex 5390 . . . . . . 7 {𝐶, {𝐵}} ∈ V
3130, 7preqr2 4808 . . . . . 6 ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
32 snex 5389 . . . . . . 7 {𝐵} ∈ V
33 snex 5389 . . . . . . 7 {𝐷} ∈ V
3432, 33preqr2 4808 . . . . . 6 ({𝐶, {𝐵}} = {𝐶, {𝐷}} → {𝐵} = {𝐷})
3531, 34syl 17 . . . . 5 ({{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → {𝐵} = {𝐷})
3629, 35syl6com 37 . . . 4 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} → {𝐵} = {𝐷}))
3720, 36jcai 518 . . 3 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} → ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
38 preq2 4696 . . . . 5 ({𝐵} = {𝐷} → {𝐶, {𝐵}} = {𝐶, {𝐷}})
3938preq2d 4702 . . . 4 ({𝐵} = {𝐷} → {{𝐶}, {𝐶, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4027, 39sylan9eq 2793 . . 3 (({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}) → {{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}})
4137, 40impbii 208 . 2 ({{𝐴}, {𝐴, {𝐵}}} = {{𝐶}, {𝐶, {𝐷}}} ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
423, 41bitri 275 1 (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wo 846   = wceq 1542  cun 3909  wss 3911  {csn 4587  {cpr 4589  caltop 34587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-sn 4588  df-pr 4590  df-altop 34589
This theorem is referenced by:  altopeq12  34593  altopth1  34596  altopth2  34597  altopthg  34598  altopthbg  34599
  Copyright terms: Public domain W3C validator