Proof of Theorem nosupinfsep
Step | Hyp | Ref
| Expression |
1 | | ssun1 4106 |
. . . . . . . 8
⊢ dom 𝑆 ⊆ (dom 𝑆 ∪ dom 𝑇) |
2 | | resabs1 5921 |
. . . . . . . 8
⊢ (dom
𝑆 ⊆ (dom 𝑆 ∪ dom 𝑇) → ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) = (𝑊 ↾ dom 𝑆)) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) = (𝑊 ↾ dom 𝑆) |
4 | 3 | breq1i 5081 |
. . . . . 6
⊢ (((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ↔ (𝑊 ↾ dom 𝑆) <s 𝑆) |
5 | 4 | notbii 320 |
. . . . 5
⊢ (¬
((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ↔ ¬ (𝑊 ↾ dom 𝑆) <s 𝑆) |
6 | | ssun2 4107 |
. . . . . . . 8
⊢ dom 𝑇 ⊆ (dom 𝑆 ∪ dom 𝑇) |
7 | | resabs1 5921 |
. . . . . . . 8
⊢ (dom
𝑇 ⊆ (dom 𝑆 ∪ dom 𝑇) → ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇) = (𝑊 ↾ dom 𝑇)) |
8 | 6, 7 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇) = (𝑊 ↾ dom 𝑇) |
9 | 8 | breq2i 5082 |
. . . . . 6
⊢ (𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇) ↔ 𝑇 <s (𝑊 ↾ dom 𝑇)) |
10 | 9 | notbii 320 |
. . . . 5
⊢ (¬
𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇) ↔ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇)) |
11 | 5, 10 | anbi12i 627 |
. . . 4
⊢ ((¬
((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇)) ↔ (¬ (𝑊 ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇))) |
12 | 11 | bicomi 223 |
. . 3
⊢ ((¬
(𝑊 ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇)) ↔ (¬ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇))) |
13 | 12 | a1i 11 |
. 2
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ ((¬ (𝑊 ↾
dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇)) ↔ (¬ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇)))) |
14 | | simp1l 1196 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ 𝐴 ⊆ No ) |
15 | | simp1r 1197 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ 𝐴 ∈
V) |
16 | | simp3 1137 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ 𝑊 ∈ No ) |
17 | | nosupinfsep.1 |
. . . . 5
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
18 | 17 | nosupbnd2 33919 |
. . . 4
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈ V
∧ 𝑊 ∈ No ) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑊 ↔ ¬ (𝑊 ↾ dom 𝑆) <s 𝑆)) |
19 | 14, 15, 16, 18 | syl3anc 1370 |
. . 3
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ (∀𝑎 ∈
𝐴 𝑎 <s 𝑊 ↔ ¬ (𝑊 ↾ dom 𝑆) <s 𝑆)) |
20 | | simp2l 1198 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ 𝐵 ⊆ No ) |
21 | | simp2r 1199 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ 𝐵 ∈
V) |
22 | | nosupinfsep.2 |
. . . . 5
⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
23 | 22 | noinfbnd2 33934 |
. . . 4
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈ V
∧ 𝑊 ∈ No ) → (∀𝑏 ∈ 𝐵 𝑊 <s 𝑏 ↔ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇))) |
24 | 20, 21, 16, 23 | syl3anc 1370 |
. . 3
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ (∀𝑏 ∈
𝐵 𝑊 <s 𝑏 ↔ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇))) |
25 | 19, 24 | anbi12d 631 |
. 2
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ ((∀𝑎 ∈
𝐴 𝑎 <s 𝑊 ∧ ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏) ↔ (¬ (𝑊 ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s (𝑊 ↾ dom 𝑇)))) |
26 | 17 | nosupno 33906 |
. . . . . . . 8
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → 𝑆 ∈ No ) |
27 | | nodmon 33853 |
. . . . . . . 8
⊢ (𝑆 ∈
No → dom 𝑆
∈ On) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → dom 𝑆 ∈
On) |
29 | 28 | 3ad2ant1 1132 |
. . . . . 6
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ dom 𝑆 ∈
On) |
30 | 22 | noinfno 33921 |
. . . . . . . 8
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈
V) → 𝑇 ∈ No ) |
31 | | nodmon 33853 |
. . . . . . . 8
⊢ (𝑇 ∈
No → dom 𝑇
∈ On) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈
V) → dom 𝑇 ∈
On) |
33 | 32 | 3ad2ant2 1133 |
. . . . . 6
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ dom 𝑇 ∈
On) |
34 | | onun2 6370 |
. . . . . 6
⊢ ((dom
𝑆 ∈ On ∧ dom 𝑇 ∈ On) → (dom 𝑆 ∪ dom 𝑇) ∈ On) |
35 | 29, 33, 34 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ (dom 𝑆 ∪ dom
𝑇) ∈
On) |
36 | | noreson 33863 |
. . . . 5
⊢ ((𝑊 ∈
No ∧ (dom 𝑆
∪ dom 𝑇) ∈ On)
→ (𝑊 ↾ (dom
𝑆 ∪ dom 𝑇)) ∈
No ) |
37 | 16, 35, 36 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ (𝑊 ↾ (dom
𝑆 ∪ dom 𝑇)) ∈
No ) |
38 | 17 | nosupbnd2 33919 |
. . . 4
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈ V
∧ (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∈ No )
→ (∀𝑎 ∈
𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ ¬ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆)) |
39 | 14, 15, 37, 38 | syl3anc 1370 |
. . 3
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ (∀𝑎 ∈
𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↔ ¬ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆)) |
40 | 20, 21, 37 | 3jca 1127 |
. . . 4
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ (𝐵 ⊆ No ∧ 𝐵 ∈ V ∧ (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∈ No
)) |
41 | 22 | noinfbnd2 33934 |
. . . 4
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈ V
∧ (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∈ No )
→ (∀𝑏 ∈
𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏 ↔ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇))) |
42 | 40, 41 | syl 17 |
. . 3
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ (∀𝑏 ∈
𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏 ↔ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇))) |
43 | 39, 42 | anbi12d 631 |
. 2
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ ((∀𝑎 ∈
𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏) ↔ (¬ ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑇 <s ((𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ↾ dom 𝑇)))) |
44 | 13, 25, 43 | 3bitr4d 311 |
1
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ 𝑊 ∈ No )
→ ((∀𝑎 ∈
𝐴 𝑎 <s 𝑊 ∧ ∀𝑏 ∈ 𝐵 𝑊 <s 𝑏) ↔ (∀𝑎 ∈ 𝐴 𝑎 <s (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) ∧ ∀𝑏 ∈ 𝐵 (𝑊 ↾ (dom 𝑆 ∪ dom 𝑇)) <s 𝑏))) |