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

Theorem propssopi 5397
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.) (Proof shortened by AV, 16-Jun-2022.) (Avoid depending on this detail.)
Hypotheses
Ref Expression
snopeqop.a 𝐴 ∈ V
snopeqop.b 𝐵 ∈ V
propeqop.c 𝐶 ∈ V
propeqop.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 4801 . . 3 𝐸, 𝐹⟩ = {{𝐸}, {𝐸, 𝐹}}
43sseq2i 3995 . 2 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ ⟨𝐸, 𝐹⟩ ↔ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}})
5 sspr 4765 . . 3 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}} ↔ (({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) ∨ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}})))
6 opex 5355 . . . . . . 7 𝐴, 𝐵⟩ ∈ V
76prnz 4711 . . . . . 6 {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ≠ ∅
8 eqneqall 3027 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ≠ ∅ → 𝐴 = 𝐶))
97, 8mpi 20 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ → 𝐴 = 𝐶)
10 opex 5355 . . . . . . 7 𝐶, 𝐷⟩ ∈ V
116, 10preqsn 4791 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸}))
12 snopeqop.a . . . . . . . . 9 𝐴 ∈ V
13 snopeqop.b . . . . . . . . 9 𝐵 ∈ V
1412, 13opth 5367 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))
15 simpl 485 . . . . . . . 8 ((𝐴 = 𝐶𝐵 = 𝐷) → 𝐴 = 𝐶)
1614, 15sylbi 219 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
1716adantr 483 . . . . . 6 ((⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸}) → 𝐴 = 𝐶)
1811, 17sylbi 219 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}} → 𝐴 = 𝐶)
199, 18jaoi 853 . . . 4 (({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) → 𝐴 = 𝐶)
206, 10preqsn 4791 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}))
2115a1d 25 . . . . . . . 8 ((𝐴 = 𝐶𝐵 = 𝐷) → (⟨𝐶, 𝐷⟩ = {𝐸, 𝐹} → 𝐴 = 𝐶))
2214, 21sylbi 219 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (⟨𝐶, 𝐷⟩ = {𝐸, 𝐹} → 𝐴 = 𝐶))
2322imp 409 . . . . . 6 ((⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}) → 𝐴 = 𝐶)
2420, 23sylbi 219 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} → 𝐴 = 𝐶)
253eqcomi 2830 . . . . . . . 8 {{𝐸}, {𝐸, 𝐹}} = ⟨𝐸, 𝐹
2625eqeq2i 2834 . . . . . . 7 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} ↔ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩)
27 propeqop.c . . . . . . . 8 𝐶 ∈ V
28 propeqop.d . . . . . . . 8 𝐷 ∈ V
2912, 13, 27, 28, 1, 2propeqop 5396 . . . . . . 7 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩ ↔ ((𝐴 = 𝐶𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷𝐹 = {𝐴, 𝐵}))))
3026, 29bitri 277 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} ↔ ((𝐴 = 𝐶𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷𝐹 = {𝐴, 𝐵}))))
31 simpll 765 . . . . . 6 (((𝐴 = 𝐶𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷𝐹 = {𝐴, 𝐵}))) → 𝐴 = 𝐶)
3230, 31sylbi 219 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} → 𝐴 = 𝐶)
3324, 32jaoi 853 . . . 4 (({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}}) → 𝐴 = 𝐶)
3419, 33jaoi 853 . . 3 ((({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) ∨ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}})) → 𝐴 = 𝐶)
355, 34sylbi 219 . 2 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}} → 𝐴 = 𝐶)
364, 35sylbi 219 1 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ ⟨𝐸, 𝐹⟩ → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wo 843   = wceq 1533  wcel 2110  wne 3016  Vcvv 3494  wss 3935  c0 4290  {csn 4566  {cpr 4568  cop 4572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573
This theorem is referenced by:  iunopeqop  5410
  Copyright terms: Public domain W3C validator