Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nofulllem4 Structured version   Visualization version   GIF version

Theorem nofulllem4 31104
 Description: Lemma for nofull (future) . Show a particular abstraction is an ordinal. (Contributed by Scott Fenton, 25-Apr-2017.)
Hypothesis
Ref Expression
nofulllem4.1 𝑀 = {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}
Assertion
Ref Expression
nofulllem4 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑀 ∈ On)
Distinct variable groups:   𝑥,𝐿,𝑦,𝑎   𝑥,𝑅,𝑦,𝑎   𝑥,𝑊,𝑦   𝑥,𝑉,𝑦
Allowed substitution hints:   𝑀(𝑥,𝑦,𝑎)   𝑉(𝑎)   𝑊(𝑎)

Proof of Theorem nofulllem4
StepHypRef Expression
1 nofulllem4.1 . 2 𝑀 = {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)}
2 unexg 6857 . . . . . . 7 ((𝐿𝑉𝑅𝑊) → (𝐿𝑅) ∈ V)
3 nobndlem1 31091 . . . . . . . 8 ((𝐿𝑅) ∈ V → suc ( bday “ (𝐿𝑅)) ∈ On)
4 sucelon 6909 . . . . . . . 8 ( ( bday “ (𝐿𝑅)) ∈ On ↔ suc ( bday “ (𝐿𝑅)) ∈ On)
53, 4sylibr 223 . . . . . . 7 ((𝐿𝑅) ∈ V → ( bday “ (𝐿𝑅)) ∈ On)
62, 5syl 17 . . . . . 6 ((𝐿𝑉𝑅𝑊) → ( bday “ (𝐿𝑅)) ∈ On)
76ad2ant2l 778 . . . . 5 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) → ( bday “ (𝐿𝑅)) ∈ On)
873adant3 1074 . . . 4 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → ( bday “ (𝐿𝑅)) ∈ On)
9 simprl 790 . . . . . . . . . . 11 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) → 𝑅 No )
10 simpr 476 . . . . . . . . . . 11 ((𝑥𝐿𝑦𝑅) → 𝑦𝑅)
11 ssel2 3563 . . . . . . . . . . 11 ((𝑅 No 𝑦𝑅) → 𝑦 No )
129, 10, 11syl2an 493 . . . . . . . . . 10 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) ∧ (𝑥𝐿𝑦𝑅)) → 𝑦 No )
13 sltirr 31069 . . . . . . . . . 10 (𝑦 No → ¬ 𝑦 <s 𝑦)
14 breq1 4586 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 <s 𝑦𝑦 <s 𝑦))
1514notbid 307 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (¬ 𝑥 <s 𝑦 ↔ ¬ 𝑦 <s 𝑦))
1615biimprcd 239 . . . . . . . . . . 11 𝑦 <s 𝑦 → (𝑥 = 𝑦 → ¬ 𝑥 <s 𝑦))
1716necon2ad 2797 . . . . . . . . . 10 𝑦 <s 𝑦 → (𝑥 <s 𝑦𝑥𝑦))
1812, 13, 173syl 18 . . . . . . . . 9 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) ∧ (𝑥𝐿𝑦𝑅)) → (𝑥 <s 𝑦𝑥𝑦))
1918impr 647 . . . . . . . 8 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) ∧ ((𝑥𝐿𝑦𝑅) ∧ 𝑥 <s 𝑦)) → 𝑥𝑦)
20 simpll 786 . . . . . . . . 9 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) → 𝐿 No )
21 simpll 786 . . . . . . . . 9 (((𝑥𝐿𝑦𝑅) ∧ 𝑥 <s 𝑦) → 𝑥𝐿)
22 ssun1 3738 . . . . . . . . . 10 𝐿 ⊆ (𝐿𝑅)
23 nofulllem3 31103 . . . . . . . . . 10 ((𝐿 No 𝑥𝐿𝐿 ⊆ (𝐿𝑅)) → (𝑥 ( bday “ (𝐿𝑅))) = 𝑥)
2422, 23mp3an3 1405 . . . . . . . . 9 ((𝐿 No 𝑥𝐿) → (𝑥 ( bday “ (𝐿𝑅))) = 𝑥)
2520, 21, 24syl2an 493 . . . . . . . 8 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) ∧ ((𝑥𝐿𝑦𝑅) ∧ 𝑥 <s 𝑦)) → (𝑥 ( bday “ (𝐿𝑅))) = 𝑥)
26 simplr 788 . . . . . . . . 9 (((𝑥𝐿𝑦𝑅) ∧ 𝑥 <s 𝑦) → 𝑦𝑅)
27 ssun2 3739 . . . . . . . . . 10 𝑅 ⊆ (𝐿𝑅)
28 nofulllem3 31103 . . . . . . . . . 10 ((𝑅 No 𝑦𝑅𝑅 ⊆ (𝐿𝑅)) → (𝑦 ( bday “ (𝐿𝑅))) = 𝑦)
2927, 28mp3an3 1405 . . . . . . . . 9 ((𝑅 No 𝑦𝑅) → (𝑦 ( bday “ (𝐿𝑅))) = 𝑦)
309, 26, 29syl2an 493 . . . . . . . 8 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) ∧ ((𝑥𝐿𝑦𝑅) ∧ 𝑥 <s 𝑦)) → (𝑦 ( bday “ (𝐿𝑅))) = 𝑦)
3119, 25, 303netr4d 2859 . . . . . . 7 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) ∧ ((𝑥𝐿𝑦𝑅) ∧ 𝑥 <s 𝑦)) → (𝑥 ( bday “ (𝐿𝑅))) ≠ (𝑦 ( bday “ (𝐿𝑅))))
3231expr 641 . . . . . 6 ((((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) ∧ (𝑥𝐿𝑦𝑅)) → (𝑥 <s 𝑦 → (𝑥 ( bday “ (𝐿𝑅))) ≠ (𝑦 ( bday “ (𝐿𝑅)))))
3332ralimdvva 2947 . . . . 5 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊)) → (∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦 → ∀𝑥𝐿𝑦𝑅 (𝑥 ( bday “ (𝐿𝑅))) ≠ (𝑦 ( bday “ (𝐿𝑅)))))
34333impia 1253 . . . 4 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → ∀𝑥𝐿𝑦𝑅 (𝑥 ( bday “ (𝐿𝑅))) ≠ (𝑦 ( bday “ (𝐿𝑅))))
35 reseq2 5312 . . . . . . 7 (𝑎 = ( bday “ (𝐿𝑅)) → (𝑥𝑎) = (𝑥 ( bday “ (𝐿𝑅))))
36 reseq2 5312 . . . . . . 7 (𝑎 = ( bday “ (𝐿𝑅)) → (𝑦𝑎) = (𝑦 ( bday “ (𝐿𝑅))))
3735, 36neeq12d 2843 . . . . . 6 (𝑎 = ( bday “ (𝐿𝑅)) → ((𝑥𝑎) ≠ (𝑦𝑎) ↔ (𝑥 ( bday “ (𝐿𝑅))) ≠ (𝑦 ( bday “ (𝐿𝑅)))))
38372ralbidv 2972 . . . . 5 (𝑎 = ( bday “ (𝐿𝑅)) → (∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎) ↔ ∀𝑥𝐿𝑦𝑅 (𝑥 ( bday “ (𝐿𝑅))) ≠ (𝑦 ( bday “ (𝐿𝑅)))))
3938rspcev 3282 . . . 4 (( ( bday “ (𝐿𝑅)) ∈ On ∧ ∀𝑥𝐿𝑦𝑅 (𝑥 ( bday “ (𝐿𝑅))) ≠ (𝑦 ( bday “ (𝐿𝑅)))) → ∃𝑎 ∈ On ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎))
408, 34, 39syl2anc 691 . . 3 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → ∃𝑎 ∈ On ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎))
41 onintrab2 6894 . . 3 (∃𝑎 ∈ On ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎) ↔ {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} ∈ On)
4240, 41sylib 207 . 2 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → {𝑎 ∈ On ∣ ∀𝑥𝐿𝑦𝑅 (𝑥𝑎) ≠ (𝑦𝑎)} ∈ On)
431, 42syl5eqel 2692 1 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → 𝑀 ∈ On)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∪ cuni 4372  ∩ cint 4410   class class class wbr 4583   ↾ cres 5040   “ cima 5041  Oncon0 5640  suc csuc 5642   No csur 31037
 Copyright terms: Public domain W3C validator