Proof of Theorem noeta2
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. 2
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → ((𝐴 ⊆ No
∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)) |
2 | | bdayfo 33525 |
. . . . . . 7
⊢ bday : No –onto→On |
3 | | fofun 6593 |
. . . . . . 7
⊢ ( bday : No –onto→On → Fun
bday ) |
4 | 2, 3 | ax-mp 5 |
. . . . . 6
⊢ Fun bday |
5 | | simp1r 1199 |
. . . . . . 7
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → 𝐴 ∈ 𝑉) |
6 | | simp2r 1201 |
. . . . . . 7
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → 𝐵 ∈ 𝑊) |
7 | | unexg 7492 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
8 | 5, 6, 7 | syl2anc 587 |
. . . . . 6
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → (𝐴 ∪ 𝐵) ∈ V) |
9 | | funimaexg 6425 |
. . . . . 6
⊢ ((Fun
bday ∧ (𝐴 ∪ 𝐵) ∈ V) → (
bday “ (𝐴
∪ 𝐵)) ∈
V) |
10 | 4, 8, 9 | sylancr 590 |
. . . . 5
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → ( bday
“ (𝐴 ∪ 𝐵)) ∈ V) |
11 | 10 | uniexd 7488 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → ∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ V) |
12 | | imassrn 5914 |
. . . . . . 7
⊢ ( bday “ (𝐴 ∪ 𝐵)) ⊆ ran bday
|
13 | | forn 6595 |
. . . . . . . 8
⊢ ( bday : No –onto→On → ran
bday = On) |
14 | 2, 13 | ax-mp 5 |
. . . . . . 7
⊢ ran bday = On |
15 | 12, 14 | sseqtri 3913 |
. . . . . 6
⊢ ( bday “ (𝐴 ∪ 𝐵)) ⊆ On |
16 | | ssorduni 7521 |
. . . . . 6
⊢ (( bday “ (𝐴 ∪ 𝐵)) ⊆ On → Ord ∪ ( bday “ (𝐴 ∪ 𝐵))) |
17 | 15, 16 | ax-mp 5 |
. . . . 5
⊢ Ord ∪ ( bday “ (𝐴 ∪ 𝐵)) |
18 | | elon2 6183 |
. . . . 5
⊢ (∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ On ↔ (Ord ∪ ( bday “ (𝐴 ∪ 𝐵)) ∧ ∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ V)) |
19 | 17, 18 | mpbiran 709 |
. . . 4
⊢ (∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ On ↔ ∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ V) |
20 | 11, 19 | sylibr 237 |
. . 3
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → ∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ On) |
21 | | sucelon 7553 |
. . 3
⊢ (∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ On ↔ suc ∪ ( bday “ (𝐴 ∪ 𝐵)) ∈ On) |
22 | 20, 21 | sylib 221 |
. 2
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → suc ∪
( bday “ (𝐴 ∪ 𝐵)) ∈ On) |
23 | | onsucuni 7564 |
. . 3
⊢ (( bday “ (𝐴 ∪ 𝐵)) ⊆ On → (
bday “ (𝐴
∪ 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |
24 | 15, 23 | mp1i 13 |
. 2
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → ( bday
“ (𝐴 ∪ 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) |
25 | | noeta 33591 |
. 2
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) ∧ (suc ∪
( bday “ (𝐴 ∪ 𝐵)) ∈ On ∧ (
bday “ (𝐴
∪ 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) → ∃𝑧 ∈ No
(∀𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |
26 | 1, 22, 24, 25 | syl12anc 836 |
1
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) → ∃𝑧 ∈ No
(∀𝑥 ∈ 𝐴 𝑥 <s 𝑧 ∧ ∀𝑦 ∈ 𝐵 𝑧 <s 𝑦 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |