Proof of Theorem nosupbnd1lem6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp2l 1199 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → 𝐴 ⊆  No
) | 
| 2 |  | simp3 1138 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → 𝑈 ∈ 𝐴) | 
| 3 | 1, 2 | sseldd 3983 | . . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → 𝑈 ∈  No
) | 
| 4 |  | nofv 27703 | . . . . 5
⊢ (𝑈 ∈ 
No  → ((𝑈‘dom 𝑆) = ∅ ∨ (𝑈‘dom 𝑆) = 1o ∨ (𝑈‘dom 𝑆) = 2o)) | 
| 5 | 3, 4 | syl 17 | . . . 4
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → ((𝑈‘dom 𝑆) = ∅ ∨ (𝑈‘dom 𝑆) = 1o ∨ (𝑈‘dom 𝑆) = 2o)) | 
| 6 |  | 3oran 1108 | . . . 4
⊢ (((𝑈‘dom 𝑆) = ∅ ∨ (𝑈‘dom 𝑆) = 1o ∨ (𝑈‘dom 𝑆) = 2o) ↔ ¬ (¬
(𝑈‘dom 𝑆) = ∅ ∧ ¬ (𝑈‘dom 𝑆) = 1o ∧ ¬ (𝑈‘dom 𝑆) = 2o)) | 
| 7 | 5, 6 | sylib 218 | . . 3
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → ¬ (¬ (𝑈‘dom 𝑆) = ∅ ∧ ¬ (𝑈‘dom 𝑆) = 1o ∧ ¬ (𝑈‘dom 𝑆) = 2o)) | 
| 8 |  | simpl1 1191 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → ¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 9 |  | simpl2 1192 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → (𝐴 ⊆  No 
∧ 𝐴 ∈
V)) | 
| 10 |  | simpl3 1193 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → 𝑈 ∈ 𝐴) | 
| 11 |  | simpr 484 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → (𝑈 ↾ dom 𝑆) = 𝑆) | 
| 12 |  | nosupbnd1.1 | . . . . . . 7
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) | 
| 13 | 12 | nosupbnd1lem4 27757 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
(𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ ∅) | 
| 14 | 8, 9, 10, 11, 13 | syl112anc 1375 | . . . . 5
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → (𝑈‘dom 𝑆) ≠ ∅) | 
| 15 | 14 | neneqd 2944 | . . . 4
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → ¬ (𝑈‘dom 𝑆) = ∅) | 
| 16 | 12 | nosupbnd1lem5 27758 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
(𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ 1o) | 
| 17 | 8, 9, 10, 11, 16 | syl112anc 1375 | . . . . 5
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → (𝑈‘dom 𝑆) ≠ 1o) | 
| 18 | 17 | neneqd 2944 | . . . 4
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → ¬ (𝑈‘dom 𝑆) = 1o) | 
| 19 | 12 | nosupbnd1lem3 27756 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
(𝑈 ∈ 𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ 2o) | 
| 20 | 8, 9, 10, 11, 19 | syl112anc 1375 | . . . . 5
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → (𝑈‘dom 𝑆) ≠ 2o) | 
| 21 | 20 | neneqd 2944 | . . . 4
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → ¬ (𝑈‘dom 𝑆) = 2o) | 
| 22 | 15, 18, 21 | 3jca 1128 | . . 3
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) ∧ (𝑈 ↾ dom 𝑆) = 𝑆) → (¬ (𝑈‘dom 𝑆) = ∅ ∧ ¬ (𝑈‘dom 𝑆) = 1o ∧ ¬ (𝑈‘dom 𝑆) = 2o)) | 
| 23 | 7, 22 | mtand 815 | . 2
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → ¬ (𝑈 ↾ dom 𝑆) = 𝑆) | 
| 24 | 12 | nosupbnd1lem1 27754 | . 2
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆)) | 
| 25 | 12 | nosupno 27749 | . . . . . 6
⊢ ((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) → 𝑆 ∈  No ) | 
| 26 | 25 | 3ad2ant2 1134 | . . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → 𝑆 ∈  No
) | 
| 27 |  | nodmon 27696 | . . . . 5
⊢ (𝑆 ∈ 
No  → dom 𝑆
∈ On) | 
| 28 | 26, 27 | syl 17 | . . . 4
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → dom 𝑆 ∈ On) | 
| 29 |  | noreson 27706 | . . . 4
⊢ ((𝑈 ∈ 
No  ∧ dom 𝑆
∈ On) → (𝑈
↾ dom 𝑆) ∈  No ) | 
| 30 | 3, 28, 29 | syl2anc 584 | . . 3
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → (𝑈 ↾ dom 𝑆) ∈  No
) | 
| 31 |  | sltso 27722 | . . . 4
⊢  <s Or
 No | 
| 32 |  | solin 5618 | . . . 4
⊢ (( <s
Or  No  ∧ ((𝑈 ↾ dom 𝑆) ∈  No 
∧ 𝑆 ∈  No )) → ((𝑈 ↾ dom 𝑆) <s 𝑆 ∨ (𝑈 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑈 ↾ dom 𝑆))) | 
| 33 | 31, 32 | mpan 690 | . . 3
⊢ (((𝑈 ↾ dom 𝑆) ∈  No 
∧ 𝑆 ∈  No ) → ((𝑈 ↾ dom 𝑆) <s 𝑆 ∨ (𝑈 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑈 ↾ dom 𝑆))) | 
| 34 | 30, 26, 33 | syl2anc 584 | . 2
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → ((𝑈 ↾ dom 𝑆) <s 𝑆 ∨ (𝑈 ↾ dom 𝑆) = 𝑆 ∨ 𝑆 <s (𝑈 ↾ dom 𝑆))) | 
| 35 | 23, 24, 34 | ecase23d 1474 | 1
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
𝑈 ∈ 𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆) |