Proof of Theorem nofulllem2
Step | Hyp | Ref
| Expression |
1 | | nobnddown 31100 |
. . 3
⊢ ((𝑅 ⊆
No ∧ 𝑅 ∈
𝑊) → ∃𝑧 ∈
No (∀𝑦
∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝑅))) |
2 | 1 | 3ad2ant2 1076 |
. 2
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∃𝑧 ∈ No
(∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝑅))) |
3 | | rzal 4025 |
. . . . . 6
⊢ (𝐿 = ∅ → ∀𝑥 ∈ 𝐿 𝑥 <s 𝑧) |
4 | 3 | biantrurd 528 |
. . . . 5
⊢ (𝐿 = ∅ → (∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ↔ (∀𝑥 ∈ 𝐿 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝑅 𝑧 <s 𝑦))) |
5 | | uneq1 3722 |
. . . . . . . . . . 11
⊢ (𝐿 = ∅ → (𝐿 ∪ 𝑅) = (∅ ∪ 𝑅)) |
6 | | uncom 3719 |
. . . . . . . . . . . 12
⊢ (∅
∪ 𝑅) = (𝑅 ∪ ∅) |
7 | | un0 3919 |
. . . . . . . . . . . 12
⊢ (𝑅 ∪ ∅) = 𝑅 |
8 | 6, 7 | eqtri 2632 |
. . . . . . . . . . 11
⊢ (∅
∪ 𝑅) = 𝑅 |
9 | 5, 8 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝐿 = ∅ → (𝐿 ∪ 𝑅) = 𝑅) |
10 | 9 | imaeq2d 5385 |
. . . . . . . . 9
⊢ (𝐿 = ∅ → ( bday “ (𝐿 ∪ 𝑅)) = ( bday
“ 𝑅)) |
11 | 10 | unieqd 4382 |
. . . . . . . 8
⊢ (𝐿 = ∅ → ∪ ( bday “ (𝐿 ∪ 𝑅)) = ∪ ( bday “ 𝑅)) |
12 | | suceq 5707 |
. . . . . . . 8
⊢ (∪ ( bday “ (𝐿 ∪ 𝑅)) = ∪ ( bday “ 𝑅) → suc ∪
( bday “ (𝐿 ∪ 𝑅)) = suc ∪ ( bday “ 𝑅)) |
13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ (𝐿 = ∅ → suc ∪ ( bday “ (𝐿 ∪ 𝑅)) = suc ∪ ( bday “ 𝑅)) |
14 | 13 | sseq2d 3596 |
. . . . . 6
⊢ (𝐿 = ∅ → (( bday ‘𝑧) ⊆ suc ∪
( bday “ (𝐿 ∪ 𝑅)) ↔ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝑅))) |
15 | 14 | bicomd 212 |
. . . . 5
⊢ (𝐿 = ∅ → (( bday ‘𝑧) ⊆ suc ∪
( bday “ 𝑅) ↔ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐿 ∪ 𝑅)))) |
16 | 4, 15 | anbi12d 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 “
(𝐿 ∪ 𝑅)))) |
18 | 16, 17 | syl6bbr 277 |
. . 3
⊢ (𝐿 = ∅ →
((∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝑅)) ↔ (∀𝑥 ∈ 𝐿 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐿 ∪ 𝑅))))) |
19 | 18 | rexbidv 3034 |
. 2
⊢ (𝐿 = ∅ → (∃𝑧 ∈
No (∀𝑦
∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝑅)) ↔ ∃𝑧 ∈
No (∀𝑥
∈ 𝐿 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐿 ∪ 𝑅))))) |
20 | 2, 19 | syl5ib 233 |
1
⊢ (𝐿 = ∅ → (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∃𝑧 ∈ No
(∀𝑥 ∈ 𝐿 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐿 ∪ 𝑅))))) |