Proof of Theorem nosupbnd1lem2
Step | Hyp | Ref
| Expression |
1 | | simp3rr 1246 |
. . . 4
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → ¬ 𝑊 <s 𝑈) |
2 | | simp2l 1198 |
. . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → 𝐴 ⊆ No
) |
3 | | simp3rl 1245 |
. . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → 𝑊 ∈ 𝐴) |
4 | 2, 3 | sseldd 3922 |
. . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → 𝑊 ∈ No
) |
5 | | simp3ll 1243 |
. . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → 𝑈 ∈ 𝐴) |
6 | 2, 5 | sseldd 3922 |
. . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → 𝑈 ∈ No
) |
7 | | nosupbnd1.1 |
. . . . . . . 8
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
8 | 7 | nosupno 33906 |
. . . . . . 7
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → 𝑆 ∈ No ) |
9 | 8 | 3ad2ant2 1133 |
. . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → 𝑆 ∈ No
) |
10 | | nodmon 33853 |
. . . . . 6
⊢ (𝑆 ∈
No → dom 𝑆
∈ On) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → dom 𝑆 ∈ On) |
12 | | sltres 33865 |
. . . . 5
⊢ ((𝑊 ∈
No ∧ 𝑈 ∈
No ∧ dom 𝑆 ∈ On) → ((𝑊 ↾ dom 𝑆) <s (𝑈 ↾ dom 𝑆) → 𝑊 <s 𝑈)) |
13 | 4, 6, 11, 12 | syl3anc 1370 |
. . . 4
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → ((𝑊 ↾ dom 𝑆) <s (𝑈 ↾ dom 𝑆) → 𝑊 <s 𝑈)) |
14 | 1, 13 | mtod 197 |
. . 3
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → ¬ (𝑊 ↾ dom 𝑆) <s (𝑈 ↾ dom 𝑆)) |
15 | | simp3lr 1244 |
. . . 4
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → (𝑈 ↾ dom 𝑆) = 𝑆) |
16 | 15 | breq2d 5086 |
. . 3
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → ((𝑊 ↾ dom 𝑆) <s (𝑈 ↾ dom 𝑆) ↔ (𝑊 ↾ dom 𝑆) <s 𝑆)) |
17 | 14, 16 | mtbid 324 |
. 2
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → ¬ (𝑊 ↾ dom 𝑆) <s 𝑆) |
18 | 7 | nosupbnd1lem1 33911 |
. . 3
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
𝑊 ∈ 𝐴) → ¬ 𝑆 <s (𝑊 ↾ dom 𝑆)) |
19 | 3, 18 | syld3an3 1408 |
. 2
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → ¬ 𝑆 <s (𝑊 ↾ dom 𝑆)) |
20 | | noreson 33863 |
. . . 4
⊢ ((𝑊 ∈
No ∧ dom 𝑆
∈ On) → (𝑊
↾ dom 𝑆) ∈ No ) |
21 | 4, 11, 20 | syl2anc 584 |
. . 3
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → (𝑊 ↾ dom 𝑆) ∈ No
) |
22 | | sltso 33879 |
. . . 4
⊢ <s Or
No |
23 | | sotrieq2 5533 |
. . . 4
⊢ (( <s
Or No ∧ ((𝑊 ↾ dom 𝑆) ∈ No
∧ 𝑆 ∈ No )) → ((𝑊 ↾ dom 𝑆) = 𝑆 ↔ (¬ (𝑊 ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑆 <s (𝑊 ↾ dom 𝑆)))) |
24 | 22, 23 | mpan 687 |
. . 3
⊢ (((𝑊 ↾ dom 𝑆) ∈ No
∧ 𝑆 ∈ No ) → ((𝑊 ↾ dom 𝑆) = 𝑆 ↔ (¬ (𝑊 ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑆 <s (𝑊 ↾ dom 𝑆)))) |
25 | 21, 9, 24 | syl2anc 584 |
. 2
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → ((𝑊 ↾ dom 𝑆) = 𝑆 ↔ (¬ (𝑊 ↾ dom 𝑆) <s 𝑆 ∧ ¬ 𝑆 <s (𝑊 ↾ dom 𝑆)))) |
26 | 17, 19, 25 | mpbir2and 710 |
1
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V) ∧
((𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈))) → (𝑊 ↾ dom 𝑆) = 𝑆) |