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

Theorem propssopi 5390
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 4796 . . 3 𝐸, 𝐹⟩ = {{𝐸}, {𝐸, 𝐹}}
43sseq2i 3995 . 2 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ ⟨𝐸, 𝐹⟩ ↔ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}})
5 sspr 4760 . . 3 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}} ↔ (({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) ∨ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}})))
6 opex 5348 . . . . . . 7 𝐴, 𝐵⟩ ∈ V
76prnz 4706 . . . . . 6 {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ≠ ∅
8 eqneqall 3027 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ≠ ∅ → 𝐴 = 𝐶))
97, 8mpi 20 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ → 𝐴 = 𝐶)
10 opex 5348 . . . . . . 7 𝐶, 𝐷⟩ ∈ V
116, 10preqsn 4786 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸}))
12 snopeqop.a . . . . . . . . 9 𝐴 ∈ V
13 snopeqop.b . . . . . . . . 9 𝐵 ∈ V
1412, 13opth 5360 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))
15 simpl 483 . . . . . . . 8 ((𝐴 = 𝐶𝐵 = 𝐷) → 𝐴 = 𝐶)
1614, 15sylbi 218 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
1716adantr 481 . . . . . 6 ((⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸}) → 𝐴 = 𝐶)
1811, 17sylbi 218 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}} → 𝐴 = 𝐶)
199, 18jaoi 851 . . . 4 (({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) → 𝐴 = 𝐶)
206, 10preqsn 4786 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}))
2115a1d 25 . . . . . . . 8 ((𝐴 = 𝐶𝐵 = 𝐷) → (⟨𝐶, 𝐷⟩ = {𝐸, 𝐹} → 𝐴 = 𝐶))
2214, 21sylbi 218 . . . . . . 7 (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (⟨𝐶, 𝐷⟩ = {𝐸, 𝐹} → 𝐴 = 𝐶))
2322imp 407 . . . . . 6 ((⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}) → 𝐴 = 𝐶)
2420, 23sylbi 218 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} → 𝐴 = 𝐶)
253eqcomi 2830 . . . . . . . 8 {{𝐸}, {𝐸, 𝐹}} = ⟨𝐸, 𝐹
2625eqeq2i 2834 . . . . . . 7 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} ↔ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩)
27 propeqop.c . . . . . . . 8 𝐶 ∈ V
28 propeqop.d . . . . . . . 8 𝐷 ∈ V
2912, 13, 27, 28, 1, 2propeqop 5389 . . . . . . 7 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩ ↔ ((𝐴 = 𝐶𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷𝐹 = {𝐴, 𝐵}))))
3026, 29bitri 276 . . . . . 6 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} ↔ ((𝐴 = 𝐶𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷𝐹 = {𝐴, 𝐵}))))
31 simpll 763 . . . . . 6 (((𝐴 = 𝐶𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷𝐹 = {𝐴, 𝐵}))) → 𝐴 = 𝐶)
3230, 31sylbi 218 . . . . 5 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} → 𝐴 = 𝐶)
3324, 32jaoi 851 . . . 4 (({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}}) → 𝐴 = 𝐶)
3419, 33jaoi 851 . . 3 ((({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) ∨ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}})) → 𝐴 = 𝐶)
355, 34sylbi 218 . 2 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}} → 𝐴 = 𝐶)
364, 35sylbi 218 1 ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ ⟨𝐸, 𝐹⟩ → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 841   = wceq 1528  wcel 2105  wne 3016  Vcvv 3495  wss 3935  c0 4290  {csn 4559  {cpr 4561  cop 4565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566
This theorem is referenced by:  iunopeqop  5403
  Copyright terms: Public domain W3C validator