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

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

Proof of Theorem nofulllem1
StepHypRef Expression
1 nobndup 30934 . . 3 ((𝐿 No 𝐿𝑉) → ∃𝑧 No (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ( bday 𝑧) ⊆ suc ( bday 𝐿)))
213ad2ant1 1074 . 2 (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → ∃𝑧 No (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ( bday 𝑧) ⊆ suc ( bday 𝐿)))
3 raleq 3019 . . . . . . 7 (𝑅 = ∅ → (∀𝑦𝑅 𝑧 <s 𝑦 ↔ ∀𝑦 ∈ ∅ 𝑧 <s 𝑦))
4 uneq2 3627 . . . . . . . . . . . 12 (𝑅 = ∅ → (𝐿𝑅) = (𝐿 ∪ ∅))
5 un0 3822 . . . . . . . . . . . 12 (𝐿 ∪ ∅) = 𝐿
64, 5syl6eq 2564 . . . . . . . . . . 11 (𝑅 = ∅ → (𝐿𝑅) = 𝐿)
76imaeq2d 5276 . . . . . . . . . 10 (𝑅 = ∅ → ( bday “ (𝐿𝑅)) = ( bday 𝐿))
87unieqd 4280 . . . . . . . . 9 (𝑅 = ∅ → ( bday “ (𝐿𝑅)) = ( bday 𝐿))
9 suceq 5595 . . . . . . . . 9 ( ( bday “ (𝐿𝑅)) = ( bday 𝐿) → suc ( bday “ (𝐿𝑅)) = suc ( bday 𝐿))
108, 9syl 17 . . . . . . . 8 (𝑅 = ∅ → suc ( bday “ (𝐿𝑅)) = suc ( bday 𝐿))
1110sseq2d 3500 . . . . . . 7 (𝑅 = ∅ → (( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)) ↔ ( bday 𝑧) ⊆ suc ( bday 𝐿)))
123, 11anbi12d 742 . . . . . 6 (𝑅 = ∅ → ((∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅))) ↔ (∀𝑦 ∈ ∅ 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday 𝐿))))
13 ral0 3931 . . . . . . 7 𝑦 ∈ ∅ 𝑧 <s 𝑦
1413biantrur 525 . . . . . 6 (( bday 𝑧) ⊆ suc ( bday 𝐿) ↔ (∀𝑦 ∈ ∅ 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday 𝐿)))
1512, 14syl6rbbr 277 . . . . 5 (𝑅 = ∅ → (( bday 𝑧) ⊆ suc ( bday 𝐿) ↔ (∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)))))
1615anbi2d 735 . . . 4 (𝑅 = ∅ → ((∀𝑥𝐿 𝑥 <s 𝑧 ∧ ( bday 𝑧) ⊆ suc ( bday 𝐿)) ↔ (∀𝑥𝐿 𝑥 <s 𝑧 ∧ (∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅))))))
17 3anass 1034 . . . 4 ((∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅))) ↔ (∀𝑥𝐿 𝑥 <s 𝑧 ∧ (∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)))))
1816, 17syl6bbr 276 . . 3 (𝑅 = ∅ → ((∀𝑥𝐿 𝑥 <s 𝑧 ∧ ( bday 𝑧) ⊆ suc ( bday 𝐿)) ↔ (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)))))
1918rexbidv 2938 . 2 (𝑅 = ∅ → (∃𝑧 No (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ( bday 𝑧) ⊆ suc ( bday 𝐿)) ↔ ∃𝑧 No (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)))))
202, 19syl5ib 232 1 (𝑅 = ∅ → (((𝐿 No 𝐿𝑉) ∧ (𝑅 No 𝑅𝑊) ∧ ∀𝑥𝐿𝑦𝑅 𝑥 <s 𝑦) → ∃𝑧 No (∀𝑥𝐿 𝑥 <s 𝑧 ∧ ∀𝑦𝑅 𝑧 <s 𝑦 ∧ ( bday 𝑧) ⊆ suc ( bday “ (𝐿𝑅)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030   = wceq 1474   ∈ wcel 1938  ∀wral 2800  ∃wrex 2801   ∪ cun 3442   ⊆ wss 3444  ∅c0 3777  ∪ cuni 4270   class class class wbr 4481   “ cima 4935  suc csuc 5532  ‘cfv 5689   No csur 30872
 Copyright terms: Public domain W3C validator