| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1l 1198 | . . 3
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → 𝑈 ∈ 𝐴) | 
| 2 |  | simp3 1139 | . . 3
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) | 
| 3 |  | breq1 5146 | . . . 4
⊢ (𝑎 = 𝑈 → (𝑎 <s 𝑍 ↔ 𝑈 <s 𝑍)) | 
| 4 | 3 | rspcv 3618 | . . 3
⊢ (𝑈 ∈ 𝐴 → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 → 𝑈 <s 𝑍)) | 
| 5 | 1, 2, 4 | sylc 65 | . 2
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → 𝑈 <s 𝑍) | 
| 6 |  | simpl21 1252 | . . . . 5
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝐴 ⊆  No
) | 
| 7 |  | simpl1l 1225 | . . . . 5
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 ∈ 𝐴) | 
| 8 | 6, 7 | sseldd 3984 | . . . 4
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 ∈  No
) | 
| 9 |  | simpl23 1254 | . . . 4
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑍 ∈  No
) | 
| 10 |  | simp21 1207 | . . . . . . . . . 10
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → 𝐴 ⊆  No
) | 
| 11 | 10, 1 | sseldd 3984 | . . . . . . . . 9
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → 𝑈 ∈  No
) | 
| 12 |  | sltso 27721 | . . . . . . . . . 10
⊢  <s Or
 No | 
| 13 |  | sonr 5616 | . . . . . . . . . 10
⊢ (( <s
Or  No  ∧ 𝑈 ∈  No )
→ ¬ 𝑈 <s 𝑈) | 
| 14 | 12, 13 | mpan 690 | . . . . . . . . 9
⊢ (𝑈 ∈ 
No  → ¬ 𝑈
<s 𝑈) | 
| 15 | 11, 14 | syl 17 | . . . . . . . 8
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ¬ 𝑈 <s 𝑈) | 
| 16 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑈 = 𝑍 → (𝑈 <s 𝑈 ↔ 𝑈 <s 𝑍)) | 
| 17 | 16 | notbid 318 | . . . . . . . 8
⊢ (𝑈 = 𝑍 → (¬ 𝑈 <s 𝑈 ↔ ¬ 𝑈 <s 𝑍)) | 
| 18 | 15, 17 | syl5ibcom 245 | . . . . . . 7
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → (𝑈 = 𝑍 → ¬ 𝑈 <s 𝑍)) | 
| 19 | 18 | con2d 134 | . . . . . 6
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → (𝑈 <s 𝑍 → ¬ 𝑈 = 𝑍)) | 
| 20 | 19 | imp 406 | . . . . 5
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ 𝑈 = 𝑍) | 
| 21 | 20 | neqned 2947 | . . . 4
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 ≠ 𝑍) | 
| 22 |  | nosepssdm 27731 | . . . 4
⊢ ((𝑈 ∈ 
No  ∧ 𝑍 ∈
 No  ∧ 𝑈 ≠ 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈) | 
| 23 | 8, 9, 21, 22 | syl3anc 1373 | . . 3
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈) | 
| 24 |  | nosepon 27710 | . . . . . 6
⊢ ((𝑈 ∈ 
No  ∧ 𝑍 ∈
 No  ∧ 𝑈 ≠ 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On) | 
| 25 | 8, 9, 21, 24 | syl3anc 1373 | . . . . 5
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On) | 
| 26 |  | nodmon 27695 | . . . . . 6
⊢ (𝑈 ∈ 
No  → dom 𝑈
∈ On) | 
| 27 | 8, 26 | syl 17 | . . . . 5
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → dom 𝑈 ∈ On) | 
| 28 |  | onsseleq 6425 | . . . . 5
⊢ ((∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 ↔ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈))) | 
| 29 | 25, 27, 28 | syl2anc 584 | . . . 4
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 ↔ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈))) | 
| 30 | 8 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 ∈  No
) | 
| 31 | 9 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑍 ∈  No
) | 
| 32 | 21 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 ≠ 𝑍) | 
| 33 | 30, 31, 32, 24 | syl3anc 1373 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On) | 
| 34 |  | onelon 6409 | . . . . . . . . . . . . . . . 16
⊢ ((∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ On) | 
| 35 | 33, 34 | sylan 580 | . . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ On) | 
| 36 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) | 
| 37 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑞 → (𝑈‘𝑥) = (𝑈‘𝑞)) | 
| 38 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑞 → (𝑍‘𝑥) = (𝑍‘𝑞)) | 
| 39 | 37, 38 | neeq12d 3002 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑞 → ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑈‘𝑞) ≠ (𝑍‘𝑞))) | 
| 40 | 39 | onnminsb 7819 | . . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ On → (𝑞 ∈ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))) | 
| 41 | 35, 36, 40 | sylc 65 | . . . . . . . . . . . . . 14
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) | 
| 42 |  | df-ne 2941 | . . . . . . . . . . . . . . 15
⊢ ((𝑈‘𝑞) ≠ (𝑍‘𝑞) ↔ ¬ (𝑈‘𝑞) = (𝑍‘𝑞)) | 
| 43 | 42 | con2bii 357 | . . . . . . . . . . . . . 14
⊢ ((𝑈‘𝑞) = (𝑍‘𝑞) ↔ ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) | 
| 44 | 41, 43 | sylibr 234 | . . . . . . . . . . . . 13
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → (𝑈‘𝑞) = (𝑍‘𝑞)) | 
| 45 |  | simplr 769 | . . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) | 
| 46 | 27 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → dom 𝑈 ∈ On) | 
| 48 |  | ontr1 6430 | . . . . . . . . . . . . . . . 16
⊢ (dom
𝑈 ∈ On → ((𝑞 ∈ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)) | 
| 49 | 47, 48 | syl 17 | . . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)) | 
| 50 | 36, 45, 49 | mp2and 699 | . . . . . . . . . . . . . 14
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ dom 𝑈) | 
| 51 | 50 | fvresd 6926 | . . . . . . . . . . . . 13
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍‘𝑞)) | 
| 52 | 44, 51 | eqtr4d 2780 | . . . . . . . . . . . 12
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞)) | 
| 53 | 52 | ralrimiva 3146 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞)) | 
| 54 |  | simplr 769 | . . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 <s 𝑍) | 
| 55 |  | sltval2 27701 | . . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ 
No  ∧ 𝑍 ∈
 No ) → (𝑈 <s 𝑍 ↔ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑍‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) | 
| 56 | 30, 31, 55 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑍‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) | 
| 57 | 54, 56 | mpbid 232 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑍‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) | 
| 58 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) | 
| 59 | 58 | fvresd 6926 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) | 
| 60 | 57, 59 | breqtrrd 5171 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝑍 ↾ dom 𝑈)‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) | 
| 61 |  | raleq 3323 | . . . . . . . . . . . . 13
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ↔ ∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))) | 
| 62 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (𝑈‘𝑝) = (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) | 
| 63 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) | 
| 64 | 62, 63 | breq12d 5156 | . . . . . . . . . . . . 13
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((𝑈‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝑍 ↾ dom 𝑈)‘𝑝) ↔ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝑍 ↾ dom 𝑈)‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) | 
| 65 | 61, 64 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝑍 ↾ dom 𝑈)‘𝑝)) ↔ (∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝑍 ↾ dom 𝑈)‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})))) | 
| 66 | 65 | rspcev 3622 | . . . . . . . . . . 11
⊢ ((∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ (∀𝑞 ∈ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝑍 ↾ dom 𝑈)‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) → ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝑍 ↾ dom 𝑈)‘𝑝))) | 
| 67 | 33, 53, 60, 66 | syl12anc 837 | . . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝑍 ↾ dom 𝑈)‘𝑝))) | 
| 68 |  | noreson 27705 | . . . . . . . . . . . 12
⊢ ((𝑍 ∈ 
No  ∧ dom 𝑈
∈ On) → (𝑍
↾ dom 𝑈) ∈  No ) | 
| 69 | 31, 46, 68 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) ∈  No
) | 
| 70 |  | sltval 27692 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ 
No  ∧ (𝑍 ↾
dom 𝑈) ∈  No ) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝑍 ↾ dom 𝑈)‘𝑝)))) | 
| 71 | 30, 69, 70 | syl2anc 584 | . . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝑍 ↾ dom 𝑈)‘𝑝)))) | 
| 72 | 67, 71 | mpbird 257 | . . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 <s (𝑍 ↾ dom 𝑈)) | 
| 73 |  | df-res 5697 | . . . . . . . . . . . . 13
⊢
({〈dom 𝑈,
2o〉} ↾ dom 𝑈) = ({〈dom 𝑈, 2o〉} ∩ (dom 𝑈 × V)) | 
| 74 |  | 2on 8520 | . . . . . . . . . . . . . . . 16
⊢
2o ∈ On | 
| 75 |  | xpsng 7159 | . . . . . . . . . . . . . . . 16
⊢ ((dom
𝑈 ∈ On ∧
2o ∈ On) → ({dom 𝑈} × {2o}) = {〈dom
𝑈,
2o〉}) | 
| 76 | 46, 74, 75 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({dom 𝑈} × {2o}) = {〈dom
𝑈,
2o〉}) | 
| 77 | 76 | ineq1d 4219 | . . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2o}) ∩ (dom 𝑈 × V)) = ({〈dom 𝑈, 2o〉} ∩
(dom 𝑈 ×
V))) | 
| 78 |  | incom 4209 | . . . . . . . . . . . . . . . 16
⊢ ({dom
𝑈} ∩ dom 𝑈) = (dom 𝑈 ∩ {dom 𝑈}) | 
| 79 |  | nodmord 27698 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ 
No  → Ord dom 𝑈) | 
| 80 |  | ordirr 6402 | . . . . . . . . . . . . . . . . . 18
⊢ (Ord dom
𝑈 → ¬ dom 𝑈 ∈ dom 𝑈) | 
| 81 | 30, 79, 80 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈) | 
| 82 |  | disjsn 4711 | . . . . . . . . . . . . . . . . 17
⊢ ((dom
𝑈 ∩ {dom 𝑈}) = ∅ ↔ ¬ dom
𝑈 ∈ dom 𝑈) | 
| 83 | 81, 82 | sylibr 234 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (dom 𝑈 ∩ {dom 𝑈}) = ∅) | 
| 84 | 78, 83 | eqtrid 2789 | . . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({dom 𝑈} ∩ dom 𝑈) = ∅) | 
| 85 |  | xpdisj1 6181 | . . . . . . . . . . . . . . 15
⊢ (({dom
𝑈} ∩ dom 𝑈) = ∅ → (({dom 𝑈} × {2o}) ∩
(dom 𝑈 × V)) =
∅) | 
| 86 | 84, 85 | syl 17 | . . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2o}) ∩ (dom 𝑈 × V)) =
∅) | 
| 87 | 77, 86 | eqtr3d 2779 | . . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({〈dom 𝑈, 2o〉} ∩ (dom 𝑈 × V)) =
∅) | 
| 88 | 73, 87 | eqtrid 2789 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({〈dom 𝑈, 2o〉} ↾ dom 𝑈) = ∅) | 
| 89 | 88 | uneq2d 4168 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({〈dom 𝑈, 2o〉} ↾ dom 𝑈)) = ((𝑈 ↾ dom 𝑈) ∪ ∅)) | 
| 90 |  | resundir 6012 | . . . . . . . . . . 11
⊢ ((𝑈 ∪ {〈dom 𝑈, 2o〉}) ↾
dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({〈dom 𝑈, 2o〉} ↾ dom 𝑈)) | 
| 91 |  | un0 4394 | . . . . . . . . . . . 12
⊢ ((𝑈 ↾ dom 𝑈) ∪ ∅) = (𝑈 ↾ dom 𝑈) | 
| 92 | 91 | eqcomi 2746 | . . . . . . . . . . 11
⊢ (𝑈 ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ∅) | 
| 93 | 89, 90, 92 | 3eqtr4g 2802 | . . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {〈dom 𝑈, 2o〉}) ↾ dom 𝑈) = (𝑈 ↾ dom 𝑈)) | 
| 94 |  | nofun 27694 | . . . . . . . . . . 11
⊢ (𝑈 ∈ 
No  → Fun 𝑈) | 
| 95 |  | funrel 6583 | . . . . . . . . . . 11
⊢ (Fun
𝑈 → Rel 𝑈) | 
| 96 |  | resdm 6044 | . . . . . . . . . . 11
⊢ (Rel
𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈) | 
| 97 | 30, 94, 95, 96 | 4syl 19 | . . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈) | 
| 98 | 93, 97 | eqtrd 2777 | . . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {〈dom 𝑈, 2o〉}) ↾ dom 𝑈) = 𝑈) | 
| 99 |  | sssucid 6464 | . . . . . . . . . 10
⊢ dom 𝑈 ⊆ suc dom 𝑈 | 
| 100 |  | resabs1 6024 | . . . . . . . . . 10
⊢ (dom
𝑈 ⊆ suc dom 𝑈 → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈)) | 
| 101 | 99, 100 | mp1i 13 | . . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈)) | 
| 102 | 72, 98, 101 | 3brtr4d 5175 | . . . . . . . 8
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {〈dom 𝑈, 2o〉}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈)) | 
| 103 | 74 | elexi 3503 | . . . . . . . . . . . . 13
⊢
2o ∈ V | 
| 104 | 103 | prid2 4763 | . . . . . . . . . . . 12
⊢
2o ∈ {1o, 2o} | 
| 105 | 104 | noextend 27711 | . . . . . . . . . . 11
⊢ (𝑈 ∈ 
No  → (𝑈 ∪
{〈dom 𝑈,
2o〉}) ∈  No
) | 
| 106 | 8, 105 | syl 17 | . . . . . . . . . 10
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑈 ∪ {〈dom 𝑈, 2o〉}) ∈  No ) | 
| 107 | 106 | adantr 480 | . . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {〈dom 𝑈, 2o〉}) ∈  No ) | 
| 108 |  | onsucb 7837 | . . . . . . . . . . . 12
⊢ (dom
𝑈 ∈ On ↔ suc dom
𝑈 ∈
On) | 
| 109 | 27, 108 | sylib 218 | . . . . . . . . . . 11
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → suc dom 𝑈 ∈ On) | 
| 110 |  | noreson 27705 | . . . . . . . . . . 11
⊢ ((𝑍 ∈ 
No  ∧ suc dom 𝑈
∈ On) → (𝑍
↾ suc dom 𝑈) ∈
 No ) | 
| 111 | 9, 109, 110 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑍 ↾ suc dom 𝑈) ∈  No
) | 
| 112 | 111 | adantr 480 | . . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈  No
) | 
| 113 |  | sltres 27707 | . . . . . . . . 9
⊢ (((𝑈 ∪ {〈dom 𝑈, 2o〉}) ∈
 No  ∧ (𝑍 ↾ suc dom 𝑈) ∈  No 
∧ dom 𝑈 ∈ On)
→ (((𝑈 ∪
{〈dom 𝑈,
2o〉}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) → (𝑈 ∪ {〈dom 𝑈, 2o〉}) <s (𝑍 ↾ suc dom 𝑈))) | 
| 114 | 107, 112,
46, 113 | syl3anc 1373 | . . . . . . . 8
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (((𝑈 ∪ {〈dom 𝑈, 2o〉}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) → (𝑈 ∪ {〈dom 𝑈, 2o〉}) <s (𝑍 ↾ suc dom 𝑈))) | 
| 115 | 102, 114 | mpd 15 | . . . . . . 7
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {〈dom 𝑈, 2o〉}) <s (𝑍 ↾ suc dom 𝑈)) | 
| 116 |  | soasym 5625 | . . . . . . . . 9
⊢ (( <s
Or  No  ∧ ((𝑈 ∪ {〈dom 𝑈, 2o〉}) ∈  No  ∧ (𝑍 ↾ suc dom 𝑈) ∈  No ))
→ ((𝑈 ∪ {〈dom
𝑈, 2o〉})
<s (𝑍 ↾ suc dom
𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 2o〉}))) | 
| 117 | 12, 116 | mpan 690 | . . . . . . . 8
⊢ (((𝑈 ∪ {〈dom 𝑈, 2o〉}) ∈
 No  ∧ (𝑍 ↾ suc dom 𝑈) ∈  No )
→ ((𝑈 ∪ {〈dom
𝑈, 2o〉})
<s (𝑍 ↾ suc dom
𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 2o〉}))) | 
| 118 | 107, 112,
117 | syl2anc 584 | . . . . . . 7
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {〈dom 𝑈, 2o〉}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 2o〉}))) | 
| 119 | 115, 118 | mpd 15 | . . . . . 6
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 2o〉})) | 
| 120 |  | df-suc 6390 | . . . . . . . . . 10
⊢ suc dom
𝑈 = (dom 𝑈 ∪ {dom 𝑈}) | 
| 121 | 120 | reseq2i 5994 | . . . . . . . . 9
⊢ (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) | 
| 122 |  | resundi 6011 | . . . . . . . . 9
⊢ (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) | 
| 123 | 121, 122 | eqtri 2765 | . . . . . . . 8
⊢ (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) | 
| 124 |  | dmres 6030 | . . . . . . . . . . 11
⊢ dom
(𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍) | 
| 125 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) | 
| 126 |  | necom 2994 | . . . . . . . . . . . . . . . 16
⊢ ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑍‘𝑥) ≠ (𝑈‘𝑥)) | 
| 127 | 126 | rabbii 3442 | . . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} | 
| 128 | 127 | inteqi 4950 | . . . . . . . . . . . . . 14
⊢ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} | 
| 129 | 9 | adantr 480 | . . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 ∈  No
) | 
| 130 | 8 | adantr 480 | . . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑈 ∈  No
) | 
| 131 | 21 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑈 ≠ 𝑍) | 
| 132 | 131 | necomd 2996 | . . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 ≠ 𝑈) | 
| 133 |  | nosepssdm 27731 | . . . . . . . . . . . . . . 15
⊢ ((𝑍 ∈ 
No  ∧ 𝑈 ∈
 No  ∧ 𝑍 ≠ 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} ⊆ dom 𝑍) | 
| 134 | 129, 130,
132, 133 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} ⊆ dom 𝑍) | 
| 135 | 128, 134 | eqsstrid 4022 | . . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑍) | 
| 136 | 125, 135 | eqsstrrd 4019 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍) | 
| 137 |  | dfss2 3969 | . . . . . . . . . . . 12
⊢ (dom
𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈) | 
| 138 | 136, 137 | sylib 218 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈) | 
| 139 | 124, 138 | eqtrid 2789 | . . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈) | 
| 140 | 139 | eleq2d 2827 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈)) | 
| 141 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈) | 
| 142 | 141 | fvresd 6926 | . . . . . . . . . . . . . 14
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍‘𝑞)) | 
| 143 | 130, 26 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ∈ On) | 
| 144 |  | onelon 6409 | . . . . . . . . . . . . . . . . 17
⊢ ((dom
𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On) | 
| 145 | 143, 144 | sylan 580 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On) | 
| 146 | 125 | eleq2d 2827 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ↔ 𝑞 ∈ dom 𝑈)) | 
| 147 | 146 | biimpar 477 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) | 
| 148 | 145, 147,
40 | sylc 65 | . . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) | 
| 149 |  | nesym 2997 | . . . . . . . . . . . . . . . 16
⊢ ((𝑈‘𝑞) ≠ (𝑍‘𝑞) ↔ ¬ (𝑍‘𝑞) = (𝑈‘𝑞)) | 
| 150 | 149 | con2bii 357 | . . . . . . . . . . . . . . 15
⊢ ((𝑍‘𝑞) = (𝑈‘𝑞) ↔ ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) | 
| 151 | 148, 150 | sylibr 234 | . . . . . . . . . . . . . 14
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍‘𝑞) = (𝑈‘𝑞)) | 
| 152 | 142, 151 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)) | 
| 153 | 152 | ex 412 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))) | 
| 154 | 140, 153 | sylbid 240 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))) | 
| 155 | 154 | ralrimiv 3145 | . . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)) | 
| 156 |  | nofun 27694 | . . . . . . . . . . . 12
⊢ (𝑍 ∈ 
No  → Fun 𝑍) | 
| 157 |  | funres 6608 | . . . . . . . . . . . 12
⊢ (Fun
𝑍 → Fun (𝑍 ↾ dom 𝑈)) | 
| 158 | 129, 156,
157 | 3syl 18 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun (𝑍 ↾ dom 𝑈)) | 
| 159 | 130, 94 | syl 17 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun 𝑈) | 
| 160 |  | eqfunfv 7056 | . . . . . . . . . . 11
⊢ ((Fun
(𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))) | 
| 161 | 158, 159,
160 | syl2anc 584 | . . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))) | 
| 162 | 139, 155,
161 | mpbir2and 713 | . . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ dom 𝑈) = 𝑈) | 
| 163 | 129, 156 | syl 17 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun 𝑍) | 
| 164 |  | funfn 6596 | . . . . . . . . . . . 12
⊢ (Fun
𝑍 ↔ 𝑍 Fn dom 𝑍) | 
| 165 | 163, 164 | sylib 218 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 Fn dom 𝑍) | 
| 166 |  | 1oex 8516 | . . . . . . . . . . . . . . . . . . 19
⊢
1o ∈ V | 
| 167 | 166 | prid1 4762 | . . . . . . . . . . . . . . . . . 18
⊢
1o ∈ {1o, 2o} | 
| 168 | 167 | nosgnn0i 27704 | . . . . . . . . . . . . . . . . 17
⊢ ∅
≠ 1o | 
| 169 |  | ndmfv 6941 | . . . . . . . . . . . . . . . . . . 19
⊢ (¬
dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅) | 
| 170 | 130, 79, 80, 169 | 4syl 19 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) = ∅) | 
| 171 | 170 | neeq1d 3000 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) ≠ 1o ↔ ∅ ≠
1o)) | 
| 172 | 168, 171 | mpbiri 258 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) ≠ 1o) | 
| 173 | 172 | neneqd 2945 | . . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 1o) | 
| 174 | 173 | intnanrd 489 | . . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅)) | 
| 175 | 173 | intnanrd 489 | . . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o)) | 
| 176 |  | simplr 769 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑈 <s 𝑍) | 
| 177 | 130, 129,
55 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑍‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) | 
| 178 | 176, 177 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑍‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) | 
| 179 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈 → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑈‘dom 𝑈)) | 
| 180 | 179 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑈‘dom 𝑈)) | 
| 181 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈 → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘dom 𝑈)) | 
| 182 | 181 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘dom 𝑈)) | 
| 183 | 178, 180,
182 | 3brtr3d 5174 | . . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑍‘dom 𝑈)) | 
| 184 |  | fvex 6919 | . . . . . . . . . . . . . . . . 17
⊢ (𝑈‘dom 𝑈) ∈ V | 
| 185 |  | fvex 6919 | . . . . . . . . . . . . . . . . 17
⊢ (𝑍‘dom 𝑈) ∈ V | 
| 186 | 184, 185 | brtp 5528 | . . . . . . . . . . . . . . . 16
⊢ ((𝑈‘dom 𝑈){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o))) | 
| 187 |  | 3orrot 1092 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o)) ↔ (((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅))) | 
| 188 |  | 3orrot 1092 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅)) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o))) | 
| 189 | 186, 187,
188 | 3bitri 297 | . . . . . . . . . . . . . . 15
⊢ ((𝑈‘dom 𝑈){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o))) | 
| 190 | 183, 189 | sylib 218 | . . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1o ∧ (𝑍‘dom 𝑈) = 2o))) | 
| 191 | 174, 175,
190 | ecase23d 1475 | . . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2o)) | 
| 192 | 191 | simprd 495 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 2o) | 
| 193 |  | ndmfv 6941 | . . . . . . . . . . . . . 14
⊢ (¬
dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅) | 
| 194 | 104 | nosgnn0i 27704 | . . . . . . . . . . . . . . . 16
⊢ ∅
≠ 2o | 
| 195 |  | neeq1 3003 | . . . . . . . . . . . . . . . 16
⊢ ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 2o ↔ ∅ ≠
2o)) | 
| 196 | 194, 195 | mpbiri 258 | . . . . . . . . . . . . . . 15
⊢ ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 2o) | 
| 197 | 196 | neneqd 2945 | . . . . . . . . . . . . . 14
⊢ ((𝑍‘dom 𝑈) = ∅ → ¬ (𝑍‘dom 𝑈) = 2o) | 
| 198 | 193, 197 | syl 17 | . . . . . . . . . . . . 13
⊢ (¬
dom 𝑈 ∈ dom 𝑍 → ¬ (𝑍‘dom 𝑈) = 2o) | 
| 199 | 198 | con4i 114 | . . . . . . . . . . . 12
⊢ ((𝑍‘dom 𝑈) = 2o → dom 𝑈 ∈ dom 𝑍) | 
| 200 | 192, 199 | syl 17 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ∈ dom 𝑍) | 
| 201 |  | fnressn 7178 | . . . . . . . . . . 11
⊢ ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {〈dom 𝑈, (𝑍‘dom 𝑈)〉}) | 
| 202 | 165, 200,
201 | syl2anc 584 | . . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {〈dom 𝑈, (𝑍‘dom 𝑈)〉}) | 
| 203 | 192 | opeq2d 4880 | . . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 〈dom 𝑈, (𝑍‘dom 𝑈)〉 = 〈dom 𝑈, 2o〉) | 
| 204 | 203 | sneqd 4638 | . . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → {〈dom 𝑈, (𝑍‘dom 𝑈)〉} = {〈dom 𝑈, 2o〉}) | 
| 205 | 202, 204 | eqtrd 2777 | . . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {〈dom 𝑈, 2o〉}) | 
| 206 | 162, 205 | uneq12d 4169 | . . . . . . . 8
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {〈dom 𝑈, 2o〉})) | 
| 207 | 123, 206 | eqtrid 2789 | . . . . . . 7
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {〈dom 𝑈, 2o〉})) | 
| 208 |  | sonr 5616 | . . . . . . . . 9
⊢ (( <s
Or  No  ∧ (𝑈 ∪ {〈dom 𝑈, 2o〉}) ∈  No ) → ¬ (𝑈 ∪ {〈dom 𝑈, 2o〉}) <s (𝑈 ∪ {〈dom 𝑈,
2o〉})) | 
| 209 | 12, 208 | mpan 690 | . . . . . . . 8
⊢ ((𝑈 ∪ {〈dom 𝑈, 2o〉}) ∈
 No  → ¬ (𝑈 ∪ {〈dom 𝑈, 2o〉}) <s (𝑈 ∪ {〈dom 𝑈,
2o〉})) | 
| 210 | 130, 105,
209 | 3syl 18 | . . . . . . 7
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {〈dom 𝑈, 2o〉}) <s (𝑈 ∪ {〈dom 𝑈,
2o〉})) | 
| 211 | 207, 210 | eqnbrtrd 5161 | . . . . . 6
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 2o〉})) | 
| 212 | 119, 211 | jaodan 960 | . . . . 5
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈)) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 2o〉})) | 
| 213 | 212 | ex 412 | . . . 4
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ((∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 2o〉}))) | 
| 214 | 29, 213 | sylbid 240 | . . 3
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 2o〉}))) | 
| 215 | 23, 214 | mpd 15 | . 2
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 2o〉})) | 
| 216 | 5, 215 | mpdan 687 | 1
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆  No 
∧ 𝐴 ∈ V ∧
𝑍 ∈  No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 2o〉})) |