Proof of Theorem nofulllem1
Step | Hyp | Ref
| Expression |
1 | | nobndup 31099 |
. . 3
⊢ ((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) → ∃𝑧 ∈
No (∀𝑥
∈ 𝐿 𝑥 <s 𝑧 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝐿))) |
2 | 1 | 3ad2ant1 1075 |
. 2
⊢ (((𝐿 ⊆
No ∧ 𝐿 ∈
𝑉) ∧ (𝑅 ⊆ No
∧ 𝑅 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐿 ∀𝑦 ∈ 𝑅 𝑥 <s 𝑦) → ∃𝑧 ∈ No
(∀𝑥 ∈ 𝐿 𝑥 <s 𝑧 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝐿))) |
3 | | raleq 3115 |
. . . . . . 7
⊢ (𝑅 = ∅ → (∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ↔ ∀𝑦 ∈ ∅ 𝑧 <s 𝑦)) |
4 | | uneq2 3723 |
. . . . . . . . . . . 12
⊢ (𝑅 = ∅ → (𝐿 ∪ 𝑅) = (𝐿 ∪ ∅)) |
5 | | un0 3919 |
. . . . . . . . . . . 12
⊢ (𝐿 ∪ ∅) = 𝐿 |
6 | 4, 5 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑅 = ∅ → (𝐿 ∪ 𝑅) = 𝐿) |
7 | 6 | imaeq2d 5385 |
. . . . . . . . . 10
⊢ (𝑅 = ∅ → ( bday “ (𝐿 ∪ 𝑅)) = ( bday
“ 𝐿)) |
8 | 7 | unieqd 4382 |
. . . . . . . . 9
⊢ (𝑅 = ∅ → ∪ ( bday “ (𝐿 ∪ 𝑅)) = ∪ ( bday “ 𝐿)) |
9 | | suceq 5707 |
. . . . . . . . 9
⊢ (∪ ( bday “ (𝐿 ∪ 𝑅)) = ∪ ( bday “ 𝐿) → suc ∪
( bday “ (𝐿 ∪ 𝑅)) = suc ∪ ( bday “ 𝐿)) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (𝑅 = ∅ → suc ∪ ( bday “ (𝐿 ∪ 𝑅)) = suc ∪ ( bday “ 𝐿)) |
11 | 10 | sseq2d 3596 |
. . . . . . 7
⊢ (𝑅 = ∅ → (( bday ‘𝑧) ⊆ suc ∪
( bday “ (𝐿 ∪ 𝑅)) ↔ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝐿))) |
12 | 3, 11 | anbi12d 743 |
. . . . . 6
⊢ (𝑅 = ∅ →
((∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐿 ∪ 𝑅))) ↔ (∀𝑦 ∈ ∅ 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝐿)))) |
13 | | ral0 4028 |
. . . . . . 7
⊢
∀𝑦 ∈
∅ 𝑧 <s 𝑦 |
14 | 13 | biantrur 526 |
. . . . . 6
⊢ (( bday ‘𝑧) ⊆ suc ∪
( bday “ 𝐿) ↔ (∀𝑦 ∈ ∅ 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝐿))) |
15 | 12, 14 | syl6rbbr 278 |
. . . . 5
⊢ (𝑅 = ∅ → (( bday ‘𝑧) ⊆ suc ∪
( bday “ 𝐿) ↔ (∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐿 ∪ 𝑅))))) |
16 | 15 | anbi2d 736 |
. . . 4
⊢ (𝑅 = ∅ →
((∀𝑥 ∈ 𝐿 𝑥 <s 𝑧 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
𝐿)) ↔ (∀𝑥 ∈ 𝐿 𝑥 <s 𝑧 ∧ (∀𝑦 ∈ 𝑅 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐿 ∪ 𝑅)))))) |
17 | | 3anass 1035 |
. . . 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 “
(𝐿 ∪ 𝑅))))) |