Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fnwe2lem3 Structured version   Visualization version   GIF version

Theorem fnwe2lem3 38142
Description: Lemma for fnwe2 38143. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.)
Hypotheses
Ref Expression
fnwe2.su (𝑧 = (𝐹𝑥) → 𝑆 = 𝑈)
fnwe2.t 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹𝑥)𝑅(𝐹𝑦) ∨ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥𝑈𝑦))}
fnwe2.s ((𝜑𝑥𝐴) → 𝑈 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑥)})
fnwe2.f (𝜑 → (𝐹𝐴):𝐴𝐵)
fnwe2.r (𝜑𝑅 We 𝐵)
fnwe2lem3.a (𝜑𝑎𝐴)
fnwe2lem3.b (𝜑𝑏𝐴)
Assertion
Ref Expression
fnwe2lem3 (𝜑 → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
Distinct variable groups:   𝑦,𝑈,𝑧,𝑎,𝑏   𝑥,𝑆,𝑦,𝑎,𝑏   𝑥,𝑅,𝑦,𝑎,𝑏   𝜑,𝑥,𝑦,𝑧   𝑥,𝐴,𝑦,𝑧,𝑎,𝑏   𝑥,𝐹,𝑦,𝑧,𝑎,𝑏   𝑇,𝑎,𝑏   𝐵,𝑎,𝑏
Allowed substitution hints:   𝜑(𝑎,𝑏)   𝐵(𝑥,𝑦,𝑧)   𝑅(𝑧)   𝑆(𝑧)   𝑇(𝑥,𝑦,𝑧)   𝑈(𝑥)

Proof of Theorem fnwe2lem3
StepHypRef Expression
1 orc 399 . . . . 5 ((𝐹𝑎)𝑅(𝐹𝑏) → ((𝐹𝑎)𝑅(𝐹𝑏) ∨ ((𝐹𝑎) = (𝐹𝑏) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏)))
21adantl 473 . . . 4 ((𝜑 ∧ (𝐹𝑎)𝑅(𝐹𝑏)) → ((𝐹𝑎)𝑅(𝐹𝑏) ∨ ((𝐹𝑎) = (𝐹𝑏) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏)))
3 fnwe2.su . . . . 5 (𝑧 = (𝐹𝑥) → 𝑆 = 𝑈)
4 fnwe2.t . . . . 5 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹𝑥)𝑅(𝐹𝑦) ∨ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥𝑈𝑦))}
53, 4fnwe2val 38139 . . . 4 (𝑎𝑇𝑏 ↔ ((𝐹𝑎)𝑅(𝐹𝑏) ∨ ((𝐹𝑎) = (𝐹𝑏) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏)))
62, 5sylibr 224 . . 3 ((𝜑 ∧ (𝐹𝑎)𝑅(𝐹𝑏)) → 𝑎𝑇𝑏)
763mix1d 1421 . 2 ((𝜑 ∧ (𝐹𝑎)𝑅(𝐹𝑏)) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
8 simplr 809 . . . . . . 7 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏) → (𝐹𝑎) = (𝐹𝑏))
9 simpr 479 . . . . . . 7 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏) → 𝑎(𝐹𝑎) / 𝑧𝑆𝑏)
108, 9jca 555 . . . . . 6 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏) → ((𝐹𝑎) = (𝐹𝑏) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏))
1110olcd 407 . . . . 5 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏) → ((𝐹𝑎)𝑅(𝐹𝑏) ∨ ((𝐹𝑎) = (𝐹𝑏) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏)))
1211, 5sylibr 224 . . . 4 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏) → 𝑎𝑇𝑏)
13123mix1d 1421 . . 3 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑎(𝐹𝑎) / 𝑧𝑆𝑏) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
14 3mix2 1416 . . . 4 (𝑎 = 𝑏 → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
1514adantl 473 . . 3 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑎 = 𝑏) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
16 simplr 809 . . . . . . . 8 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑏(𝐹𝑎) / 𝑧𝑆𝑎) → (𝐹𝑎) = (𝐹𝑏))
1716eqcomd 2766 . . . . . . 7 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑏(𝐹𝑎) / 𝑧𝑆𝑎) → (𝐹𝑏) = (𝐹𝑎))
18 csbeq1 3677 . . . . . . . . . 10 ((𝐹𝑎) = (𝐹𝑏) → (𝐹𝑎) / 𝑧𝑆 = (𝐹𝑏) / 𝑧𝑆)
1918adantl 473 . . . . . . . . 9 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹𝑎) / 𝑧𝑆 = (𝐹𝑏) / 𝑧𝑆)
2019breqd 4815 . . . . . . . 8 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝑏(𝐹𝑎) / 𝑧𝑆𝑎𝑏(𝐹𝑏) / 𝑧𝑆𝑎))
2120biimpa 502 . . . . . . 7 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑏(𝐹𝑎) / 𝑧𝑆𝑎) → 𝑏(𝐹𝑏) / 𝑧𝑆𝑎)
2217, 21jca 555 . . . . . 6 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑏(𝐹𝑎) / 𝑧𝑆𝑎) → ((𝐹𝑏) = (𝐹𝑎) ∧ 𝑏(𝐹𝑏) / 𝑧𝑆𝑎))
2322olcd 407 . . . . 5 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑏(𝐹𝑎) / 𝑧𝑆𝑎) → ((𝐹𝑏)𝑅(𝐹𝑎) ∨ ((𝐹𝑏) = (𝐹𝑎) ∧ 𝑏(𝐹𝑏) / 𝑧𝑆𝑎)))
243, 4fnwe2val 38139 . . . . 5 (𝑏𝑇𝑎 ↔ ((𝐹𝑏)𝑅(𝐹𝑎) ∨ ((𝐹𝑏) = (𝐹𝑎) ∧ 𝑏(𝐹𝑏) / 𝑧𝑆𝑎)))
2523, 24sylibr 224 . . . 4 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑏(𝐹𝑎) / 𝑧𝑆𝑎) → 𝑏𝑇𝑎)
26253mix3d 1423 . . 3 (((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) ∧ 𝑏(𝐹𝑎) / 𝑧𝑆𝑎) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
27 fnwe2lem3.a . . . . . . 7 (𝜑𝑎𝐴)
28 fnwe2.s . . . . . . . 8 ((𝜑𝑥𝐴) → 𝑈 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑥)})
293, 4, 28fnwe2lem1 38140 . . . . . . 7 ((𝜑𝑎𝐴) → (𝐹𝑎) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)})
3027, 29mpdan 705 . . . . . 6 (𝜑(𝐹𝑎) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)})
31 weso 5257 . . . . . 6 ((𝐹𝑎) / 𝑧𝑆 We {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)} → (𝐹𝑎) / 𝑧𝑆 Or {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)})
3230, 31syl 17 . . . . 5 (𝜑(𝐹𝑎) / 𝑧𝑆 Or {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)})
3332adantr 472 . . . 4 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹𝑎) / 𝑧𝑆 Or {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)})
3427adantr 472 . . . . 5 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎𝐴)
35 eqidd 2761 . . . . 5 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹𝑎) = (𝐹𝑎))
36 fveq2 6353 . . . . . . 7 (𝑦 = 𝑎 → (𝐹𝑦) = (𝐹𝑎))
3736eqeq1d 2762 . . . . . 6 (𝑦 = 𝑎 → ((𝐹𝑦) = (𝐹𝑎) ↔ (𝐹𝑎) = (𝐹𝑎)))
3837elrab 3504 . . . . 5 (𝑎 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)} ↔ (𝑎𝐴 ∧ (𝐹𝑎) = (𝐹𝑎)))
3934, 35, 38sylanbrc 701 . . . 4 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑎 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)})
40 fnwe2lem3.b . . . . . 6 (𝜑𝑏𝐴)
4140adantr 472 . . . . 5 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑏𝐴)
42 simpr 479 . . . . . 6 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹𝑎) = (𝐹𝑏))
4342eqcomd 2766 . . . . 5 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝐹𝑏) = (𝐹𝑎))
44 fveq2 6353 . . . . . . 7 (𝑦 = 𝑏 → (𝐹𝑦) = (𝐹𝑏))
4544eqeq1d 2762 . . . . . 6 (𝑦 = 𝑏 → ((𝐹𝑦) = (𝐹𝑎) ↔ (𝐹𝑏) = (𝐹𝑎)))
4645elrab 3504 . . . . 5 (𝑏 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)} ↔ (𝑏𝐴 ∧ (𝐹𝑏) = (𝐹𝑎)))
4741, 43, 46sylanbrc 701 . . . 4 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → 𝑏 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)})
48 solin 5210 . . . 4 (((𝐹𝑎) / 𝑧𝑆 Or {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)} ∧ (𝑎 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)} ∧ 𝑏 ∈ {𝑦𝐴 ∣ (𝐹𝑦) = (𝐹𝑎)})) → (𝑎(𝐹𝑎) / 𝑧𝑆𝑏𝑎 = 𝑏𝑏(𝐹𝑎) / 𝑧𝑆𝑎))
4933, 39, 47, 48syl12anc 1475 . . 3 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝑎(𝐹𝑎) / 𝑧𝑆𝑏𝑎 = 𝑏𝑏(𝐹𝑎) / 𝑧𝑆𝑎))
5013, 15, 26, 49mpjao3dan 1544 . 2 ((𝜑 ∧ (𝐹𝑎) = (𝐹𝑏)) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
51 orc 399 . . . . 5 ((𝐹𝑏)𝑅(𝐹𝑎) → ((𝐹𝑏)𝑅(𝐹𝑎) ∨ ((𝐹𝑏) = (𝐹𝑎) ∧ 𝑏(𝐹𝑏) / 𝑧𝑆𝑎)))
5251adantl 473 . . . 4 ((𝜑 ∧ (𝐹𝑏)𝑅(𝐹𝑎)) → ((𝐹𝑏)𝑅(𝐹𝑎) ∨ ((𝐹𝑏) = (𝐹𝑎) ∧ 𝑏(𝐹𝑏) / 𝑧𝑆𝑎)))
5352, 24sylibr 224 . . 3 ((𝜑 ∧ (𝐹𝑏)𝑅(𝐹𝑎)) → 𝑏𝑇𝑎)
54533mix3d 1423 . 2 ((𝜑 ∧ (𝐹𝑏)𝑅(𝐹𝑎)) → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
55 fnwe2.r . . . 4 (𝜑𝑅 We 𝐵)
56 weso 5257 . . . 4 (𝑅 We 𝐵𝑅 Or 𝐵)
5755, 56syl 17 . . 3 (𝜑𝑅 Or 𝐵)
58 fvres 6369 . . . . 5 (𝑎𝐴 → ((𝐹𝐴)‘𝑎) = (𝐹𝑎))
5927, 58syl 17 . . . 4 (𝜑 → ((𝐹𝐴)‘𝑎) = (𝐹𝑎))
60 fnwe2.f . . . . 5 (𝜑 → (𝐹𝐴):𝐴𝐵)
6160, 27ffvelrnd 6524 . . . 4 (𝜑 → ((𝐹𝐴)‘𝑎) ∈ 𝐵)
6259, 61eqeltrrd 2840 . . 3 (𝜑 → (𝐹𝑎) ∈ 𝐵)
63 fvres 6369 . . . . 5 (𝑏𝐴 → ((𝐹𝐴)‘𝑏) = (𝐹𝑏))
6440, 63syl 17 . . . 4 (𝜑 → ((𝐹𝐴)‘𝑏) = (𝐹𝑏))
6560, 40ffvelrnd 6524 . . . 4 (𝜑 → ((𝐹𝐴)‘𝑏) ∈ 𝐵)
6664, 65eqeltrrd 2840 . . 3 (𝜑 → (𝐹𝑏) ∈ 𝐵)
67 solin 5210 . . 3 ((𝑅 Or 𝐵 ∧ ((𝐹𝑎) ∈ 𝐵 ∧ (𝐹𝑏) ∈ 𝐵)) → ((𝐹𝑎)𝑅(𝐹𝑏) ∨ (𝐹𝑎) = (𝐹𝑏) ∨ (𝐹𝑏)𝑅(𝐹𝑎)))
6857, 62, 66, 67syl12anc 1475 . 2 (𝜑 → ((𝐹𝑎)𝑅(𝐹𝑏) ∨ (𝐹𝑎) = (𝐹𝑏) ∨ (𝐹𝑏)𝑅(𝐹𝑎)))
697, 50, 54, 68mpjao3dan 1544 1 (𝜑 → (𝑎𝑇𝑏𝑎 = 𝑏𝑏𝑇𝑎))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383  w3o 1071   = wceq 1632  wcel 2139  {crab 3054  csb 3674   class class class wbr 4804  {copab 4864   Or wor 5186   We wwe 5224  cres 5268  wf 6045  cfv 6049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057
This theorem is referenced by:  fnwe2  38143
  Copyright terms: Public domain W3C validator