| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfv 1913 | . . . . . 6
⊢
Ⅎ𝑥((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) | 
| 2 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑥𝑍 | 
| 3 |  | nosupbnd2.1 | . . . . . . . . . . 11
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) | 
| 4 |  | nfre1 3284 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 | 
| 5 |  | nfriota1 7396 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 6 | 5 | nfdm 5961 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 7 |  | nfcv 2904 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥2o | 
| 8 | 6, 7 | nfop 4888 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉 | 
| 9 | 8 | nfsn 4706 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥{〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉} | 
| 10 | 5, 9 | nfun 4169 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) | 
| 11 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥{𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} | 
| 12 |  | nfiota1 6515 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥(℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) | 
| 13 | 11, 12 | nfmpt 5248 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) | 
| 14 | 4, 10, 13 | nfif 4555 | . . . . . . . . . . 11
⊢
Ⅎ𝑥if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) | 
| 15 | 3, 14 | nfcxfr 2902 | . . . . . . . . . 10
⊢
Ⅎ𝑥𝑆 | 
| 16 | 15 | nfdm 5961 | . . . . . . . . 9
⊢
Ⅎ𝑥dom
𝑆 | 
| 17 | 2, 16 | nfres 5998 | . . . . . . . 8
⊢
Ⅎ𝑥(𝑍 ↾ dom 𝑆) | 
| 18 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑥
<s | 
| 19 | 17, 18, 15 | nfbr 5189 | . . . . . . 7
⊢
Ⅎ𝑥(𝑍 ↾ dom 𝑆) <s 𝑆 | 
| 20 | 19 | nfn 1856 | . . . . . 6
⊢
Ⅎ𝑥 ¬
(𝑍 ↾ dom 𝑆) <s 𝑆 | 
| 21 | 1, 20 | nfim 1895 | . . . . 5
⊢
Ⅎ𝑥(((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) | 
| 22 |  | simpl 482 | . . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) | 
| 23 |  | rspe 3248 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 24 | 23 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 25 |  | nomaxmo 27744 | . . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 
No  → ∃*𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 26 | 25 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 27 | 26 | ad2antrl 728 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 28 |  | reu5 3381 | . . . . . . . . . . 11
⊢
(∃!𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) | 
| 29 | 24, 27, 28 | sylanbrc 583 | . . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 30 |  | riota1 7410 | . . . . . . . . . 10
⊢
(∃!𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ↔ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)) | 
| 31 | 29, 30 | syl 17 | . . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ↔ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)) | 
| 32 | 22, 31 | mpbid 232 | . . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥) | 
| 33 |  | nosupbnd2lem1 27761 | . . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {〈dom 𝑥, 2o〉})) | 
| 34 | 33 | 3expb 1120 | . . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {〈dom 𝑥, 2o〉})) | 
| 35 |  | dmeq 5913 | . . . . . . . . . . . . 13
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = dom 𝑥) | 
| 36 |  | suceq 6449 | . . . . . . . . . . . . 13
⊢ (dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = dom 𝑥 → suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = suc dom 𝑥) | 
| 37 | 35, 36 | syl 17 | . . . . . . . . . . . 12
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = suc dom 𝑥) | 
| 38 | 37 | reseq2d 5996 | . . . . . . . . . . 11
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (𝑍 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) = (𝑍 ↾ suc dom 𝑥)) | 
| 39 |  | id 22 | . . . . . . . . . . . 12
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥) | 
| 40 | 35 | opeq1d 4878 | . . . . . . . . . . . . 13
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → 〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉 = 〈dom 𝑥,
2o〉) | 
| 41 | 40 | sneqd 4637 | . . . . . . . . . . . 12
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉} = {〈dom 𝑥,
2o〉}) | 
| 42 | 39, 41 | uneq12d 4168 | . . . . . . . . . . 11
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) = (𝑥 ∪ {〈dom 𝑥,
2o〉})) | 
| 43 | 38, 42 | breq12d 5155 | . . . . . . . . . 10
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((𝑍 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) ↔ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {〈dom 𝑥, 2o〉}))) | 
| 44 | 43 | notbid 318 | . . . . . . . . 9
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (¬ (𝑍 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) ↔ ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {〈dom 𝑥, 2o〉}))) | 
| 45 | 34, 44 | syl5ibrcom 247 | . . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ¬ (𝑍 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}))) | 
| 46 | 32, 45 | mpd 15 | . . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉})) | 
| 47 |  | iftrue 4530 | . . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉})) | 
| 48 | 3, 47 | eqtrid 2788 | . . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉})) | 
| 49 | 23, 48 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) → 𝑆 = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉})) | 
| 50 | 49 | dmeqd 5915 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) → dom 𝑆 = dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉})) | 
| 51 |  | 2on 8521 | . . . . . . . . . . . . . . 15
⊢
2o ∈ On | 
| 52 | 51 | elexi 3502 | . . . . . . . . . . . . . 14
⊢
2o ∈ V | 
| 53 | 52 | dmsnop 6235 | . . . . . . . . . . . . 13
⊢ dom
{〈dom (℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉} = {dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)} | 
| 54 | 53 | uneq2i 4164 | . . . . . . . . . . . 12
⊢ (dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) = (dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)}) | 
| 55 |  | dmun 5920 | . . . . . . . . . . . 12
⊢ dom
((℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) = (dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) | 
| 56 |  | df-suc 6389 | . . . . . . . . . . . 12
⊢ suc dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)}) | 
| 57 | 54, 55, 56 | 3eqtr4i 2774 | . . . . . . . . . . 11
⊢ dom
((℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) = suc dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 58 | 50, 57 | eqtrdi 2792 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) → dom 𝑆 = suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) | 
| 59 | 58 | reseq2d 5996 | . . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) → (𝑍 ↾ dom 𝑆) = (𝑍 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))) | 
| 60 | 59 | adantr 480 | . . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → (𝑍 ↾ dom 𝑆) = (𝑍 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))) | 
| 61 | 49 | adantr 480 | . . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → 𝑆 = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉})) | 
| 62 | 60, 61 | breq12d 5155 | . . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ((𝑍 ↾ dom 𝑆) <s 𝑆 ↔ (𝑍 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}))) | 
| 63 | 46, 62 | mtbird 325 | . . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) | 
| 64 | 63 | exp31 419 | . . . . 5
⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → (((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆))) | 
| 65 | 21, 64 | rexlimi 3258 | . . . 4
⊢
(∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → (((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)) | 
| 66 | 65 | imp 406 | . . 3
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) | 
| 67 | 3 | nosupno 27749 | . . . . . . . 8
⊢ ((𝐴 ⊆ 
No  ∧ 𝐴 ∈
V) → 𝑆 ∈  No ) | 
| 68 | 67 | 3adant3 1132 | . . . . . . 7
⊢ ((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) → 𝑆 ∈  No
) | 
| 69 | 68 | ad2antrl 728 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → 𝑆 ∈  No
) | 
| 70 |  | nodmon 27696 | . . . . . . 7
⊢ (𝑆 ∈ 
No  → dom 𝑆
∈ On) | 
| 71 | 69, 70 | syl 17 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → dom 𝑆 ∈ On) | 
| 72 |  | noreson 27706 | . . . . . 6
⊢ ((𝑆 ∈ 
No  ∧ dom 𝑆
∈ On) → (𝑆
↾ dom 𝑆) ∈  No ) | 
| 73 | 69, 71, 72 | syl2anc 584 | . . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → (𝑆 ↾ dom 𝑆) ∈  No
) | 
| 74 |  | simprl3 1220 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → 𝑍 ∈  No
) | 
| 75 |  | noreson 27706 | . . . . . 6
⊢ ((𝑍 ∈ 
No  ∧ dom 𝑆
∈ On) → (𝑍
↾ dom 𝑆) ∈  No ) | 
| 76 | 74, 71, 75 | syl2anc 584 | . . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → (𝑍 ↾ dom 𝑆) ∈  No
) | 
| 77 |  | dmres 6029 | . . . . . . 7
⊢ dom
(𝑆 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑆) | 
| 78 |  | inss2 4237 | . . . . . . 7
⊢ (dom
𝑆 ∩ dom 𝑆) ⊆ dom 𝑆 | 
| 79 | 77, 78 | eqsstri 4029 | . . . . . 6
⊢ dom
(𝑆 ↾ dom 𝑆) ⊆ dom 𝑆 | 
| 80 | 79 | a1i 11 | . . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → dom (𝑆 ↾ dom 𝑆) ⊆ dom 𝑆) | 
| 81 |  | dmres 6029 | . . . . . . 7
⊢ dom
(𝑍 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑍) | 
| 82 |  | inss1 4236 | . . . . . . 7
⊢ (dom
𝑆 ∩ dom 𝑍) ⊆ dom 𝑆 | 
| 83 | 81, 82 | eqsstri 4029 | . . . . . 6
⊢ dom
(𝑍 ↾ dom 𝑆) ⊆ dom 𝑆 | 
| 84 | 83 | a1i 11 | . . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → dom (𝑍 ↾ dom 𝑆) ⊆ dom 𝑆) | 
| 85 | 3 | nosupdm 27750 | . . . . . . . . . . 11
⊢ (¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑔 ∣ ∃𝑝 ∈ 𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))}) | 
| 86 | 85 | eqabrd 2883 | . . . . . . . . . 10
⊢ (¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → (𝑔 ∈ dom 𝑆 ↔ ∃𝑝 ∈ 𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) | 
| 87 | 86 | adantr 480 | . . . . . . . . 9
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → (𝑔 ∈ dom 𝑆 ↔ ∃𝑝 ∈ 𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) | 
| 88 |  | simprl 770 | . . . . . . . . . . . . . 14
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 ∈ 𝐴) | 
| 89 |  | simplrr 777 | . . . . . . . . . . . . . 14
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) | 
| 90 |  | breq1 5145 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑝 → (𝑎 <s 𝑍 ↔ 𝑝 <s 𝑍)) | 
| 91 | 90 | rspcv 3617 | . . . . . . . . . . . . . 14
⊢ (𝑝 ∈ 𝐴 → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 → 𝑝 <s 𝑍)) | 
| 92 | 88, 89, 91 | sylc 65 | . . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 <s 𝑍) | 
| 93 |  | simprl1 1218 | . . . . . . . . . . . . . . . 16
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → 𝐴 ⊆  No
) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐴 ⊆  No
) | 
| 95 | 94, 88 | sseldd 3983 | . . . . . . . . . . . . . 14
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 ∈  No
) | 
| 96 | 74 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 ∈  No
) | 
| 97 |  | sltso 27722 | . . . . . . . . . . . . . . 15
⊢  <s Or
 No | 
| 98 |  | soasym 5624 | . . . . . . . . . . . . . . 15
⊢ (( <s
Or  No  ∧ (𝑝 ∈  No 
∧ 𝑍 ∈  No )) → (𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝)) | 
| 99 | 97, 98 | mpan 690 | . . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ 
No  ∧ 𝑍 ∈
 No ) → (𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝)) | 
| 100 | 95, 96, 99 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝)) | 
| 101 | 92, 100 | mpd 15 | . . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ 𝑍 <s 𝑝) | 
| 102 |  | nodmon 27696 | . . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ 
No  → dom 𝑝
∈ On) | 
| 103 | 95, 102 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → dom 𝑝 ∈ On) | 
| 104 |  | simprrl 780 | . . . . . . . . . . . . . . 15
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ dom 𝑝) | 
| 105 |  | onelon 6408 | . . . . . . . . . . . . . . 15
⊢ ((dom
𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝) → 𝑔 ∈ On) | 
| 106 | 103, 104,
105 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ On) | 
| 107 |  | onsucb 7838 | . . . . . . . . . . . . . 14
⊢ (𝑔 ∈ On ↔ suc 𝑔 ∈ On) | 
| 108 | 106, 107 | sylib 218 | . . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → suc 𝑔 ∈ On) | 
| 109 |  | sltres 27708 | . . . . . . . . . . . . 13
⊢ ((𝑍 ∈ 
No  ∧ 𝑝 ∈
 No  ∧ suc 𝑔 ∈ On) → ((𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔) → 𝑍 <s 𝑝)) | 
| 110 | 96, 95, 108, 109 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ((𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔) → 𝑍 <s 𝑝)) | 
| 111 | 101, 110 | mtod 198 | . . . . . . . . . . 11
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔)) | 
| 112 |  | simpll 766 | . . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) | 
| 113 |  | simprl2 1219 | . . . . . . . . . . . . . . 15
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → 𝐴 ∈ V) | 
| 114 | 93, 113 | jca 511 | . . . . . . . . . . . . . 14
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → (𝐴 ⊆  No 
∧ 𝐴 ∈
V)) | 
| 115 | 114 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝐴 ⊆  No 
∧ 𝐴 ∈
V)) | 
| 116 |  | simprrr 781 | . . . . . . . . . . . . . 14
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) | 
| 117 |  | breq1 5145 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑞 → (𝑣 <s 𝑝 ↔ 𝑞 <s 𝑝)) | 
| 118 | 117 | notbid 318 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑞 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑞 <s 𝑝)) | 
| 119 |  | reseq1 5990 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑞 → (𝑣 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) | 
| 120 | 119 | eqeq2d 2747 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑞 → ((𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔) ↔ (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) | 
| 121 | 118, 120 | imbi12d 344 | . . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑞 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))) | 
| 122 | 121 | cbvralvw 3236 | . . . . . . . . . . . . . 14
⊢
(∀𝑣 ∈
𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) | 
| 123 | 116, 122 | sylibr 234 | . . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) | 
| 124 | 3 | nosupres 27753 | . . . . . . . . . . . . 13
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V) ∧
(𝑝 ∈ 𝐴 ∧ 𝑔 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑆 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔)) | 
| 125 | 112, 115,
88, 104, 123, 124 | syl113anc 1383 | . . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑆 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔)) | 
| 126 | 125 | breq2d 5154 | . . . . . . . . . . 11
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ((𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔) ↔ (𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔))) | 
| 127 | 111, 126 | mtbird 325 | . . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔)) | 
| 128 | 127 | rexlimdvaa 3155 | . . . . . . . . 9
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → (∃𝑝 ∈ 𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐴 (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔))) | 
| 129 | 87, 128 | sylbid 240 | . . . . . . . 8
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → (𝑔 ∈ dom 𝑆 → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔))) | 
| 130 | 129 | imp 406 | . . . . . . 7
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔)) | 
| 131 | 69 | adantr 480 | . . . . . . . . . . 11
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → 𝑆 ∈  No
) | 
| 132 |  | nodmord 27699 | . . . . . . . . . . 11
⊢ (𝑆 ∈ 
No  → Ord dom 𝑆) | 
| 133 | 131, 132 | syl 17 | . . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → Ord dom 𝑆) | 
| 134 |  | simpr 484 | . . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → 𝑔 ∈ dom 𝑆) | 
| 135 |  | ordsucss 7839 | . . . . . . . . . 10
⊢ (Ord dom
𝑆 → (𝑔 ∈ dom 𝑆 → suc 𝑔 ⊆ dom 𝑆)) | 
| 136 | 133, 134,
135 | sylc 65 | . . . . . . . . 9
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → suc 𝑔 ⊆ dom 𝑆) | 
| 137 | 136 | resabs1d 6025 | . . . . . . . 8
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) = (𝑍 ↾ suc 𝑔)) | 
| 138 | 136 | resabs1d 6025 | . . . . . . . 8
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔) = (𝑆 ↾ suc 𝑔)) | 
| 139 | 137, 138 | breq12d 5155 | . . . . . . 7
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → (((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔) ↔ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔))) | 
| 140 | 130, 139 | mtbird 325 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ¬ ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔)) | 
| 141 | 140 | ralrimiva 3145 | . . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ∀𝑔 ∈ dom 𝑆 ¬ ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔)) | 
| 142 |  | noresle 27743 | . . . . 5
⊢ ((((𝑆 ↾ dom 𝑆) ∈  No 
∧ (𝑍 ↾ dom 𝑆) ∈ 
No ) ∧ (dom (𝑆
↾ dom 𝑆) ⊆ dom
𝑆 ∧ dom (𝑍 ↾ dom 𝑆) ⊆ dom 𝑆 ∧ ∀𝑔 ∈ dom 𝑆 ¬ ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔))) → ¬ (𝑍 ↾ dom 𝑆) <s (𝑆 ↾ dom 𝑆)) | 
| 143 | 73, 76, 80, 84, 141, 142 | syl23anc 1378 | . . . 4
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s (𝑆 ↾ dom 𝑆)) | 
| 144 |  | nofun 27695 | . . . . . 6
⊢ (𝑆 ∈ 
No  → Fun 𝑆) | 
| 145 |  | funrel 6582 | . . . . . 6
⊢ (Fun
𝑆 → Rel 𝑆) | 
| 146 |  | resdm 6043 | . . . . . 6
⊢ (Rel
𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆) | 
| 147 | 69, 144, 145, 146 | 4syl 19 | . . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → (𝑆 ↾ dom 𝑆) = 𝑆) | 
| 148 | 147 | breq2d 5154 | . . . 4
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ((𝑍 ↾ dom 𝑆) <s (𝑆 ↾ dom 𝑆) ↔ (𝑍 ↾ dom 𝑆) <s 𝑆)) | 
| 149 | 143, 148 | mtbid 324 | . . 3
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) | 
| 150 | 66, 149 | pm2.61ian 811 | . 2
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) | 
| 151 |  | simpll1 1212 | . . . . . 6
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → 𝐴 ⊆  No
) | 
| 152 |  | simpll2 1213 | . . . . . 6
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → 𝐴 ∈ V) | 
| 153 |  | simpr 484 | . . . . . 6
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) | 
| 154 | 3 | nosupbnd1 27760 | . . . . . 6
⊢ ((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑎 ∈ 𝐴) → (𝑎 ↾ dom 𝑆) <s 𝑆) | 
| 155 | 151, 152,
153, 154 | syl3anc 1372 | . . . . 5
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → (𝑎 ↾ dom 𝑆) <s 𝑆) | 
| 156 |  | simplr 768 | . . . . 5
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) | 
| 157 |  | simpl1 1191 | . . . . . . . 8
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → 𝐴 ⊆  No
) | 
| 158 | 157 | sselda 3982 | . . . . . . 7
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈  No
) | 
| 159 | 151, 152,
67 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → 𝑆 ∈  No
) | 
| 160 | 159, 70 | syl 17 | . . . . . . 7
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → dom 𝑆 ∈ On) | 
| 161 |  | noreson 27706 | . . . . . . 7
⊢ ((𝑎 ∈ 
No  ∧ dom 𝑆
∈ On) → (𝑎
↾ dom 𝑆) ∈  No ) | 
| 162 | 158, 160,
161 | syl2anc 584 | . . . . . 6
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → (𝑎 ↾ dom 𝑆) ∈  No
) | 
| 163 |  | simpll3 1214 | . . . . . . 7
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → 𝑍 ∈  No
) | 
| 164 | 163, 160,
75 | syl2anc 584 | . . . . . 6
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → (𝑍 ↾ dom 𝑆) ∈  No
) | 
| 165 |  | sotr3 5632 | . . . . . . 7
⊢ (( <s
Or  No  ∧ ((𝑎 ↾ dom 𝑆) ∈  No 
∧ 𝑆 ∈  No  ∧ (𝑍 ↾ dom 𝑆) ∈  No ))
→ (((𝑎 ↾ dom
𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆))) | 
| 166 | 97, 165 | mpan 690 | . . . . . 6
⊢ (((𝑎 ↾ dom 𝑆) ∈  No 
∧ 𝑆 ∈  No  ∧ (𝑍 ↾ dom 𝑆) ∈  No )
→ (((𝑎 ↾ dom
𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆))) | 
| 167 | 162, 159,
164, 166 | syl3anc 1372 | . . . . 5
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → (((𝑎 ↾ dom 𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆))) | 
| 168 | 155, 156,
167 | mp2and 699 | . . . 4
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆)) | 
| 169 |  | sltres 27708 | . . . . 5
⊢ ((𝑎 ∈ 
No  ∧ 𝑍 ∈
 No  ∧ dom 𝑆 ∈ On) → ((𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆) → 𝑎 <s 𝑍)) | 
| 170 | 158, 163,
160, 169 | syl3anc 1372 | . . . 4
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → ((𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆) → 𝑎 <s 𝑍)) | 
| 171 | 168, 170 | mpd 15 | . . 3
⊢ ((((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑍) | 
| 172 | 171 | ralrimiva 3145 | . 2
⊢ (((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) | 
| 173 | 150, 172 | impbida 800 | 1
⊢ ((𝐴 ⊆ 
No  ∧ 𝐴 ∈ V
∧ 𝑍 ∈  No ) → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 ↔ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)) |