Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  propssopi Structured version   Visualization version   GIF version

Theorem propssopi 4941
 Description: If a pair of ordered pairs is a subset of an ordered pair, their first components are equal. (Contributed by AV, 20-Sep-2020.)
Hypotheses
Ref Expression
snopeqop.a 𝐴 ∈ V
snopeqop.b 𝐵 ∈ V
snopeqop.c 𝐶 ∈ V
snopeqop.d 𝐷 ∈ V
propeqop.e 𝐸 ∈ V
propeqop.f 𝐹 ∈ V
Assertion
Ref Expression
propssopi ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ ⟨𝐸, 𝐹⟩ → 𝐴 = 𝐶)

Proof of Theorem propssopi
StepHypRef Expression
1 propeqop.e . . . 4 𝐸 ∈ V
2 propeqop.f . . . 4 𝐹 ∈ V
31, 2dfop 4376 . . 3 𝐸, 𝐹⟩ = {{𝐸}, {𝐸, 𝐹}}
43sseq2i 3615 . 2 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ ⟨𝐸, 𝐹⟩ ↔ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}})
5 sspr 4341 . . 3 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}} ↔ (({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) ∨ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}})))
6 opex 4903 . . . . . . 7 𝐴, 𝐵⟩ ∈ V
76prnz 4287 . . . . . 6 {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ≠ ∅
8 eqneqall 2801 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ≠ ∅ → 𝐴 = 𝐶))
97, 8mpi 20 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ → 𝐴 = 𝐶)
10 opex 4903 . . . . . . 7 𝐶, 𝐷⟩ ∈ V
11 snex 4879 . . . . . . 7 {𝐸} ∈ V
126, 10, 11preqsn 4368 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸}))
13 snopeqop.a . . . . . . . . 9 𝐴 ∈ V
14 snopeqop.b . . . . . . . . 9 𝐵 ∈ V
1513, 14opth 4915 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))
16 simpl 473 . . . . . . . 8 ((𝐴 = 𝐶𝐵 = 𝐷) → 𝐴 = 𝐶)
1715, 16sylbi 207 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
1817adantr 481 . . . . . 6 ((⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸}) → 𝐴 = 𝐶)
1912, 18sylbi 207 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}} → 𝐴 = 𝐶)
209, 19jaoi 394 . . . 4 (({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) → 𝐴 = 𝐶)
21 prex 4880 . . . . . . 7 {𝐸, 𝐹} ∈ V
226, 10, 21preqsn 4368 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}))
2316a1d 25 . . . . . . . 8 ((𝐴 = 𝐶𝐵 = 𝐷) → (⟨𝐶, 𝐷⟩ = {𝐸, 𝐹} → 𝐴 = 𝐶))
2415, 23sylbi 207 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (⟨𝐶, 𝐷⟩ = {𝐸, 𝐹} → 𝐴 = 𝐶))
2524imp 445 . . . . . 6 ((⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}) → 𝐴 = 𝐶)
2622, 25sylbi 207 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} → 𝐴 = 𝐶)
273eqcomi 2630 . . . . . . . 8 {{𝐸}, {𝐸, 𝐹}} = ⟨𝐸, 𝐹
2827eqeq2i 2633 . . . . . . 7 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} ↔ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩)
29 snopeqop.c . . . . . . . 8 𝐶 ∈ V
30 snopeqop.d . . . . . . . 8 𝐷 ∈ V
3113, 14, 29, 30, 1, 2propeqop 4940 . . . . . . 7 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩ ↔ ((𝐴 = 𝐶𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷𝐹 = {𝐴, 𝐵}))))
3228, 31bitri 264 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} ↔ ((𝐴 = 𝐶𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷𝐹 = {𝐴, 𝐵}))))
33 simpll 789 . . . . . 6 (((𝐴 = 𝐶𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷𝐹 = {𝐴, 𝐵}))) → 𝐴 = 𝐶)
3432, 33sylbi 207 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} → 𝐴 = 𝐶)
3526, 34jaoi 394 . . . 4 (({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}}) → 𝐴 = 𝐶)
3620, 35jaoi 394 . . 3 ((({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) ∨ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}})) → 𝐴 = 𝐶)
375, 36sylbi 207 . 2 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}} → 𝐴 = 𝐶)
384, 37sylbi 207 1 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ ⟨𝐸, 𝐹⟩ → 𝐴 = 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 383   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  Vcvv 3190   ⊆ wss 3560  ∅c0 3897  {csn 4155  {cpr 4157  ⟨cop 4161 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162 This theorem is referenced by:  iunopeqop  4951
 Copyright terms: Public domain W3C validator