Proof of Theorem noetalem5
Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | 1 | anim2i 593 |
. 2
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) → (𝐴 ⊆
No ∧ 𝐴 ∈
V)) |
3 | | elex 3212 |
. . 3
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) |
4 | 3 | anim2i 593 |
. 2
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈
𝑊) → (𝐵 ⊆
No ∧ 𝐵 ∈
V)) |
5 | | id 22 |
. 2
⊢
(∀𝑎 ∈
𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) |
6 | | simp1l 1085 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → 𝐴 ⊆ No
) |
7 | | simp1r 1086 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → 𝐴 ∈ V) |
8 | | simp2r 1088 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → 𝐵 ∈ V) |
9 | | noetalem.1 |
. . . . 5
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2𝑜〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
10 | | noetalem.2 |
. . . . 5
⊢ 𝑍 = (𝑆 ∪ ((suc ∪
( bday “ 𝐵) ∖ dom 𝑆) ×
{1𝑜})) |
11 | 9, 10 | noetalem1 31863 |
. . . 4
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈ V
∧ 𝐵 ∈ V) →
𝑍 ∈ No ) |
12 | 6, 7, 8, 11 | syl3anc 1326 |
. . 3
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → 𝑍 ∈ No
) |
13 | | simplll 798 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐴 ⊆ No
) |
14 | | simpllr 799 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐴 ∈ V) |
15 | | simplrr 801 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝐵 ∈ V) |
16 | | simpr 477 |
. . . . . 6
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
17 | 9, 10 | noetalem2 31864 |
. . . . . 6
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈ V
∧ 𝐵 ∈ V) ∧
𝑎 ∈ 𝐴) → 𝑎 <s 𝑍) |
18 | 13, 14, 15, 16, 17 | syl31anc 1329 |
. . . . 5
⊢ ((((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑍) |
19 | 18 | ralrimiva 2966 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) |
20 | 19 | 3adant3 1081 |
. . 3
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) |
21 | 9, 10 | noetalem3 31865 |
. . 3
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) |
22 | 9, 10 | noetalem4 31866 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V)) → (
bday ‘𝑍)
⊆ suc ∪ ( bday
“ (𝐴 ∪ 𝐵))) |
23 | 22 | 3adant3 1081 |
. . 3
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ( bday
‘𝑍) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))) |
24 | | breq2 4657 |
. . . . . 6
⊢ (𝑧 = 𝑍 → (𝑎 <s 𝑧 ↔ 𝑎 <s 𝑍)) |
25 | 24 | ralbidv 2986 |
. . . . 5
⊢ (𝑧 = 𝑍 → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑧 ↔ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) |
26 | | breq1 4656 |
. . . . . 6
⊢ (𝑧 = 𝑍 → (𝑧 <s 𝑏 ↔ 𝑍 <s 𝑏)) |
27 | 26 | ralbidv 2986 |
. . . . 5
⊢ (𝑧 = 𝑍 → (∀𝑏 ∈ 𝐵 𝑧 <s 𝑏 ↔ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) |
28 | | fveq2 6191 |
. . . . . 6
⊢ (𝑧 = 𝑍 → ( bday
‘𝑧) = ( bday ‘𝑍)) |
29 | 28 | sseq1d 3632 |
. . . . 5
⊢ (𝑧 = 𝑍 → (( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)) ↔ ( bday
‘𝑍) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |
30 | 25, 27, 29 | 3anbi123d 1399 |
. . . 4
⊢ (𝑧 = 𝑍 → ((∀𝑎 ∈ 𝐴 𝑎 <s 𝑧 ∧ ∀𝑏 ∈ 𝐵 𝑧 <s 𝑏 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏 ∧ ( bday
‘𝑍) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵))))) |
31 | 30 | rspcev 3309 |
. . 3
⊢ ((𝑍 ∈
No ∧ (∀𝑎
∈ 𝐴 𝑎 <s 𝑍 ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏 ∧ ( bday
‘𝑍) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) → ∃𝑧 ∈ No
(∀𝑎 ∈ 𝐴 𝑎 <s 𝑧 ∧ ∀𝑏 ∈ 𝐵 𝑧 <s 𝑏 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |
32 | 12, 20, 21, 23, 31 | syl13anc 1328 |
. 2
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∃𝑧 ∈ No
(∀𝑎 ∈ 𝐴 𝑎 <s 𝑧 ∧ ∀𝑏 ∈ 𝐵 𝑧 <s 𝑏 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |
33 | 2, 4, 5, 32 | syl3an 1368 |
1
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
𝑉) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑊) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 𝑎 <s 𝑏) → ∃𝑧 ∈ No
(∀𝑎 ∈ 𝐴 𝑎 <s 𝑧 ∧ ∀𝑏 ∈ 𝐵 𝑧 <s 𝑏 ∧ ( bday
‘𝑧) ⊆
suc ∪ ( bday “
(𝐴 ∪ 𝐵)))) |