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

Theorem nofulllem2 31102
 Description: Lemma for nofull (future) . The full statement of the axiom when 𝐿 is empty. (Contributed by Scott Fenton, 3-Aug-2011.)
Assertion
Ref Expression
nofulllem2 (𝐿 = ∅ → (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → ∃𝑧 No (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)))))
Distinct variable groups:   𝑦,𝑧   𝑧,𝐿   𝑥,𝐿   𝑦,𝑅,𝑧
Allowed substitution hints:   𝑅(𝑥)   𝐿(𝑦)   𝑉(𝑥,𝑦,𝑧)   𝑊(𝑥,𝑦,𝑧)

Proof of Theorem nofulllem2
StepHypRef Expression
1 nobnddown 31100 . . 3 ((𝑅 No 𝑅𝑊) → ∃𝑧 No (∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday 𝑅)))
213ad2ant2 1076 . 2 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → ∃𝑧 No (∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday 𝑅)))
3 rzal 4025 . . . . . 6 (𝐿 = ∅ → ∀𝑥𝐿 𝑥 <s 𝑧)
43biantrurd 528 . . . . 5 (𝐿 = ∅ → (∀𝑦𝑅 𝑧 <s 𝑦 ↔ (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦)))
5 uneq1 3722 . . . . . . . . . . 11 (𝐿 = ∅ → (𝐿𝑅) = (∅ ∪ 𝑅))
6 uncom 3719 . . . . . . . . . . . 12 (∅ ∪ 𝑅) = (𝑅 ∪ ∅)
7 un0 3919 . . . . . . . . . . . 12 (𝑅 ∪ ∅) = 𝑅
86, 7eqtri 2632 . . . . . . . . . . 11 (∅ ∪ 𝑅) = 𝑅
95, 8syl6eq 2660 . . . . . . . . . 10 (𝐿 = ∅ → (𝐿𝑅) = 𝑅)
109imaeq2d 5385 . . . . . . . . 9 (𝐿 = ∅ → ( bday “ (𝐿𝑅)) = ( bday 𝑅))
1110unieqd 4382 . . . . . . . 8 (𝐿 = ∅ → ( bday “ (𝐿𝑅)) = ( bday 𝑅))
12 suceq 5707 . . . . . . . 8 ( ( bday “ (𝐿𝑅)) = ( bday 𝑅) → suc ( bday “ (𝐿𝑅)) = suc ( bday 𝑅))
1311, 12syl 17 . . . . . . 7 (𝐿 = ∅ → suc ( bday “ (𝐿𝑅)) = suc ( bday 𝑅))
1413sseq2d 3596 . . . . . 6 (𝐿 = ∅ → (( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)) ↔ ( bday 𝑧) ⊆ suc ( bday 𝑅)))
1514bicomd 212 . . . . 5 (𝐿 = ∅ → (( bday 𝑧) ⊆ suc ( bday 𝑅) ↔ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅))))
164, 15anbi12d 743 . . . 4 (𝐿 = ∅ → ((∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday 𝑅)) ↔ ((∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦) ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)))))
17 df-3an 1033 . . . 4 ((∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅))) ↔ ((∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦) ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅))))
1816, 17syl6bbr 277 . . 3 (𝐿 = ∅ → ((∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday 𝑅)) ↔ (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)))))
1918rexbidv 3034 . 2 (𝐿 = ∅ → (∃𝑧 No (∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday 𝑅)) ↔ ∃𝑧 No (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)))))
202, 19syl5ib 233 1 (𝐿 = ∅ → (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → ∃𝑧 No (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  ∪ cuni 4372   class class class wbr 4583   “ cima 5041  suc csuc 5642  ‘cfv 5804   No csur 31037
 Copyright terms: Public domain W3C validator