Step | Hyp | Ref
| Expression |
1 | | simp1l 1085 |
. . 3
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → 𝑈 ∈ 𝐴) |
2 | | simp3 1063 |
. . 3
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) |
3 | | breq1 4656 |
. . . 4
⊢ (𝑎 = 𝑈 → (𝑎 <s 𝑍 ↔ 𝑈 <s 𝑍)) |
4 | 3 | rspcv 3305 |
. . 3
⊢ (𝑈 ∈ 𝐴 → (∀𝑎 ∈ 𝐴 𝑎 <s 𝑍 → 𝑈 <s 𝑍)) |
5 | 1, 2, 4 | sylc 65 |
. 2
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → 𝑈 <s 𝑍) |
6 | | simpl21 1139 |
. . . . 5
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝐴 ⊆ No
) |
7 | | simpl1l 1112 |
. . . . 5
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 ∈ 𝐴) |
8 | 6, 7 | sseldd 3604 |
. . . 4
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 ∈ No
) |
9 | | simpl23 1141 |
. . . 4
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑍 ∈ No
) |
10 | | simp21 1094 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → 𝐴 ⊆ No
) |
11 | 10, 1 | sseldd 3604 |
. . . . . . . . 9
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → 𝑈 ∈ No
) |
12 | | sltso 31827 |
. . . . . . . . . 10
⊢ <s Or
No |
13 | | sonr 5056 |
. . . . . . . . . 10
⊢ (( <s
Or No ∧ 𝑈 ∈ No )
→ ¬ 𝑈 <s 𝑈) |
14 | 12, 13 | mpan 706 |
. . . . . . . . 9
⊢ (𝑈 ∈
No → ¬ 𝑈
<s 𝑈) |
15 | 11, 14 | syl 17 |
. . . . . . . 8
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ¬ 𝑈 <s 𝑈) |
16 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑈 = 𝑍 → (𝑈 <s 𝑈 ↔ 𝑈 <s 𝑍)) |
17 | 16 | notbid 308 |
. . . . . . . 8
⊢ (𝑈 = 𝑍 → (¬ 𝑈 <s 𝑈 ↔ ¬ 𝑈 <s 𝑍)) |
18 | 15, 17 | syl5ibcom 235 |
. . . . . . 7
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → (𝑈 = 𝑍 → ¬ 𝑈 <s 𝑍)) |
19 | 18 | con2d 129 |
. . . . . 6
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → (𝑈 <s 𝑍 → ¬ 𝑈 = 𝑍)) |
20 | 19 | imp 445 |
. . . . 5
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ 𝑈 = 𝑍) |
21 | 20 | neqned 2801 |
. . . 4
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → 𝑈 ≠ 𝑍) |
22 | | nosepssdm 31836 |
. . . 4
⊢ ((𝑈 ∈
No ∧ 𝑍 ∈
No ∧ 𝑈 ≠ 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈) |
23 | 8, 9, 21, 22 | syl3anc 1326 |
. . 3
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈) |
24 | | nosepon 31818 |
. . . . . 6
⊢ ((𝑈 ∈
No ∧ 𝑍 ∈
No ∧ 𝑈 ≠ 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On) |
25 | 8, 9, 21, 24 | syl3anc 1326 |
. . . . 5
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On) |
26 | | nodmon 31803 |
. . . . . 6
⊢ (𝑈 ∈
No → dom 𝑈
∈ On) |
27 | 8, 26 | syl 17 |
. . . . 5
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → dom 𝑈 ∈ On) |
28 | | onsseleq 5765 |
. . . . 5
⊢ ((∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 ↔ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈))) |
29 | 25, 27, 28 | syl2anc 693 |
. . . 4
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 ↔ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈))) |
30 | 8 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 ∈ No
) |
31 | 9 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑍 ∈ No
) |
32 | 21 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 ≠ 𝑍) |
33 | 30, 31, 32, 24 | syl3anc 1326 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On) |
34 | | onelon 5748 |
. . . . . . . . . . . . . . . 16
⊢ ((∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ On) |
35 | 33, 34 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ On) |
36 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) |
37 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑞 → (𝑈‘𝑥) = (𝑈‘𝑞)) |
38 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑞 → (𝑍‘𝑥) = (𝑍‘𝑞)) |
39 | 37, 38 | neeq12d 2855 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑞 → ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑈‘𝑞) ≠ (𝑍‘𝑞))) |
40 | 39 | onnminsb 7004 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ On → (𝑞 ∈ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))) |
41 | 35, 36, 40 | sylc 65 |
. . . . . . . . . . . . . 14
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) |
42 | | df-ne 2795 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈‘𝑞) ≠ (𝑍‘𝑞) ↔ ¬ (𝑈‘𝑞) = (𝑍‘𝑞)) |
43 | 42 | con2bii 347 |
. . . . . . . . . . . . . 14
⊢ ((𝑈‘𝑞) = (𝑍‘𝑞) ↔ ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) |
44 | 41, 43 | sylibr 224 |
. . . . . . . . . . . . 13
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → (𝑈‘𝑞) = (𝑍‘𝑞)) |
45 | | simplr 792 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) |
46 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → dom 𝑈 ∈ On) |
48 | | ontr1 5771 |
. . . . . . . . . . . . . . . 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 715 |
. . . . . . . . . . . . . 14
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ dom 𝑈) |
51 | 50 | fvresd 6208 |
. . . . . . . . . . . . 13
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍‘𝑞)) |
52 | 44, 51 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞)) |
53 | 52 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞)) |
54 | | simplr 792 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 <s 𝑍) |
55 | | sltval2 31809 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈
No ∧ 𝑍 ∈
No ) → (𝑈 <s 𝑍 ↔ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) |
56 | 30, 31, 55 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) |
57 | 54, 56 | mpbid 222 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
58 | | simpr 477 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) |
59 | 58 | fvresd 6208 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
60 | 57, 59 | breqtrrd 4681 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
61 | | raleq 3138 |
. . . . . . . . . . . . 13
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ↔ ∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞))) |
62 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (𝑈‘𝑝) = (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
63 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
64 | 62, 63 | breq12d 4666 |
. . . . . . . . . . . . 13
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((𝑈‘𝑝){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝑍 ↾ dom 𝑈)‘𝑝) ↔ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) |
65 | 61, 64 | anbi12d 747 |
. . . . . . . . . . . 12
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘𝑝){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝑍 ↾ dom 𝑈)‘𝑝)) ↔ (∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})))) |
66 | 65 | rspcev 3309 |
. . . . . . . . . . 11
⊢ ((∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ (∀𝑞 ∈ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) → ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘𝑝){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝑍 ↾ dom 𝑈)‘𝑝))) |
67 | 33, 53, 60, 66 | syl12anc 1324 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘𝑝){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝑍 ↾ dom 𝑈)‘𝑝))) |
68 | | noreson 31813 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈
No ∧ dom 𝑈
∈ On) → (𝑍
↾ dom 𝑈) ∈ No ) |
69 | 31, 46, 68 | syl2anc 693 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No
) |
70 | | sltval 31800 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈
No ∧ (𝑍 ↾
dom 𝑈) ∈ No ) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘𝑝){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝑍 ↾ dom 𝑈)‘𝑝)))) |
71 | 30, 69, 70 | syl2anc 693 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 <s (𝑍 ↾ dom 𝑈) ↔ ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 (𝑈‘𝑞) = ((𝑍 ↾ dom 𝑈)‘𝑞) ∧ (𝑈‘𝑝){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝑍 ↾ dom 𝑈)‘𝑝)))) |
72 | 67, 71 | mpbird 247 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 <s (𝑍 ↾ dom 𝑈)) |
73 | | df-res 5126 |
. . . . . . . . . . . . 13
⊢
({〈dom 𝑈,
2𝑜〉} ↾ dom 𝑈) = ({〈dom 𝑈, 2𝑜〉} ∩ (dom
𝑈 ×
V)) |
74 | | 2on 7568 |
. . . . . . . . . . . . . . . 16
⊢
2𝑜 ∈ On |
75 | | xpsng 6406 |
. . . . . . . . . . . . . . . 16
⊢ ((dom
𝑈 ∈ On ∧
2𝑜 ∈ On) → ({dom 𝑈} × {2𝑜}) =
{〈dom 𝑈,
2𝑜〉}) |
76 | 46, 74, 75 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({dom 𝑈} × {2𝑜}) =
{〈dom 𝑈,
2𝑜〉}) |
77 | 76 | ineq1d 3813 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2𝑜}) ∩
(dom 𝑈 × V)) =
({〈dom 𝑈,
2𝑜〉} ∩ (dom 𝑈 × V))) |
78 | | incom 3805 |
. . . . . . . . . . . . . . . 16
⊢ ({dom
𝑈} ∩ dom 𝑈) = (dom 𝑈 ∩ {dom 𝑈}) |
79 | | nodmord 31806 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈
No → Ord dom 𝑈) |
80 | | ordirr 5741 |
. . . . . . . . . . . . . . . . . 18
⊢ (Ord dom
𝑈 → ¬ dom 𝑈 ∈ dom 𝑈) |
81 | 30, 79, 80 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈) |
82 | | disjsn 4246 |
. . . . . . . . . . . . . . . . 17
⊢ ((dom
𝑈 ∩ {dom 𝑈}) = ∅ ↔ ¬ dom
𝑈 ∈ dom 𝑈) |
83 | 81, 82 | sylibr 224 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (dom 𝑈 ∩ {dom 𝑈}) = ∅) |
84 | 78, 83 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({dom 𝑈} ∩ dom 𝑈) = ∅) |
85 | | xpdisj1 5555 |
. . . . . . . . . . . . . . 15
⊢ (({dom
𝑈} ∩ dom 𝑈) = ∅ → (({dom 𝑈} ×
{2𝑜}) ∩ (dom 𝑈 × V)) = ∅) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (({dom 𝑈} × {2𝑜}) ∩
(dom 𝑈 × V)) =
∅) |
87 | 77, 86 | eqtr3d 2658 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({〈dom 𝑈, 2𝑜〉} ∩ (dom
𝑈 × V)) =
∅) |
88 | 73, 87 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({〈dom 𝑈, 2𝑜〉} ↾ dom
𝑈) =
∅) |
89 | 88 | uneq2d 3767 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({〈dom 𝑈, 2𝑜〉} ↾ dom
𝑈)) = ((𝑈 ↾ dom 𝑈) ∪ ∅)) |
90 | | resundir 5411 |
. . . . . . . . . . 11
⊢ ((𝑈 ∪ {〈dom 𝑈, 2𝑜〉})
↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({〈dom 𝑈, 2𝑜〉} ↾ dom
𝑈)) |
91 | | un0 3967 |
. . . . . . . . . . . 12
⊢ ((𝑈 ↾ dom 𝑈) ∪ ∅) = (𝑈 ↾ dom 𝑈) |
92 | 91 | eqcomi 2631 |
. . . . . . . . . . 11
⊢ (𝑈 ↾ dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ∅) |
93 | 89, 90, 92 | 3eqtr4g 2681 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) ↾ dom
𝑈) = (𝑈 ↾ dom 𝑈)) |
94 | | nofun 31802 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈
No → Fun 𝑈) |
95 | 30, 94 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → Fun 𝑈) |
96 | | funrel 5905 |
. . . . . . . . . . 11
⊢ (Fun
𝑈 → Rel 𝑈) |
97 | | resdm 5441 |
. . . . . . . . . . 11
⊢ (Rel
𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈) |
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈) |
99 | 93, 98 | eqtrd 2656 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) ↾ dom
𝑈) = 𝑈) |
100 | | sssucid 5802 |
. . . . . . . . . 10
⊢ dom 𝑈 ⊆ suc dom 𝑈 |
101 | | resabs1 5427 |
. . . . . . . . . 10
⊢ (dom
𝑈 ⊆ suc dom 𝑈 → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈)) |
102 | 100, 101 | mp1i 13 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈)) |
103 | 72, 99, 102 | 3brtr4d 4685 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) ↾ dom
𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈)) |
104 | 74 | elexi 3213 |
. . . . . . . . . . . . 13
⊢
2𝑜 ∈ V |
105 | 104 | prid2 4298 |
. . . . . . . . . . . 12
⊢
2𝑜 ∈ {1𝑜,
2𝑜} |
106 | 105 | noextend 31819 |
. . . . . . . . . . 11
⊢ (𝑈 ∈
No → (𝑈 ∪
{〈dom 𝑈,
2𝑜〉}) ∈ No
) |
107 | 8, 106 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) ∈ No ) |
108 | 107 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) ∈ No ) |
109 | | sucelon 7017 |
. . . . . . . . . . . 12
⊢ (dom
𝑈 ∈ On ↔ suc dom
𝑈 ∈
On) |
110 | 27, 109 | sylib 208 |
. . . . . . . . . . 11
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → suc dom 𝑈 ∈ On) |
111 | | noreson 31813 |
. . . . . . . . . . 11
⊢ ((𝑍 ∈
No ∧ suc dom 𝑈
∈ On) → (𝑍
↾ suc dom 𝑈) ∈
No ) |
112 | 9, 110, 111 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (𝑍 ↾ suc dom 𝑈) ∈ No
) |
113 | 112 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No
) |
114 | | sltres 31815 |
. . . . . . . . 9
⊢ (((𝑈 ∪ {〈dom 𝑈, 2𝑜〉})
∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No
∧ dom 𝑈 ∈ On)
→ (((𝑈 ∪
{〈dom 𝑈,
2𝑜〉}) ↾ dom 𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) → (𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) <s (𝑍 ↾ suc dom 𝑈))) |
115 | 108, 113,
46, 114 | syl3anc 1326 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (((𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) ↾ dom
𝑈) <s ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) → (𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) <s (𝑍 ↾ suc dom 𝑈))) |
116 | 103, 115 | mpd 15 |
. . . . . . 7
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) <s (𝑍 ↾ suc dom 𝑈)) |
117 | | soasym 31657 |
. . . . . . . . 9
⊢ (( <s
Or No ∧ ((𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) ∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No ))
→ ((𝑈 ∪ {〈dom
𝑈,
2𝑜〉}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉}))) |
118 | 12, 117 | mpan 706 |
. . . . . . . 8
⊢ (((𝑈 ∪ {〈dom 𝑈, 2𝑜〉})
∈ No ∧ (𝑍 ↾ suc dom 𝑈) ∈ No )
→ ((𝑈 ∪ {〈dom
𝑈,
2𝑜〉}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉}))) |
119 | 108, 113,
118 | syl2anc 693 |
. . . . . . 7
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) <s (𝑍 ↾ suc dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉}))) |
120 | 116, 119 | mpd 15 |
. . . . . 6
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉})) |
121 | | df-suc 5729 |
. . . . . . . . . 10
⊢ suc dom
𝑈 = (dom 𝑈 ∪ {dom 𝑈}) |
122 | 121 | reseq2i 5393 |
. . . . . . . . 9
⊢ (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) |
123 | | resundi 5410 |
. . . . . . . . 9
⊢ (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) |
124 | 122, 123 | eqtri 2644 |
. . . . . . . 8
⊢ (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) |
125 | | dmres 5419 |
. . . . . . . . . . 11
⊢ dom
(𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍) |
126 | | simpr 477 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) |
127 | | necom 2847 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑍‘𝑥) ≠ (𝑈‘𝑥)) |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ On → ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑍‘𝑥) ≠ (𝑈‘𝑥))) |
129 | 128 | rabbiia 3185 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} |
130 | 129 | inteqi 4479 |
. . . . . . . . . . . . . 14
⊢ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} |
131 | 9 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 ∈ No
) |
132 | 8 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑈 ∈ No
) |
133 | 21 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑈 ≠ 𝑍) |
134 | 133 | necomd 2849 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 ≠ 𝑈) |
135 | | nosepssdm 31836 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍 ∈
No ∧ 𝑈 ∈
No ∧ 𝑍 ≠ 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} ⊆ dom 𝑍) |
136 | 131, 132,
134, 135 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} ⊆ dom 𝑍) |
137 | 130, 136 | syl5eqss 3649 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑍) |
138 | 126, 137 | eqsstr3d 3640 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍) |
139 | | df-ss 3588 |
. . . . . . . . . . . 12
⊢ (dom
𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈) |
140 | 138, 139 | sylib 208 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈) |
141 | 125, 140 | syl5eq 2668 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈) |
142 | 141 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈)) |
143 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈) |
144 | 143 | fvresd 6208 |
. . . . . . . . . . . . . 14
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍‘𝑞)) |
145 | 132, 26 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ∈ On) |
146 | | onelon 5748 |
. . . . . . . . . . . . . . . . 17
⊢ ((dom
𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On) |
147 | 145, 146 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On) |
148 | 126 | eleq2d 2687 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ↔ 𝑞 ∈ dom 𝑈)) |
149 | 148 | biimpar 502 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) |
150 | 147, 149,
40 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) |
151 | | nesym 2850 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈‘𝑞) ≠ (𝑍‘𝑞) ↔ ¬ (𝑍‘𝑞) = (𝑈‘𝑞)) |
152 | 151 | con2bii 347 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍‘𝑞) = (𝑈‘𝑞) ↔ ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) |
153 | 150, 152 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍‘𝑞) = (𝑈‘𝑞)) |
154 | 144, 153 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢
((((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)) |
155 | 154 | ex 450 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))) |
156 | 142, 155 | sylbid 230 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))) |
157 | 156 | ralrimiv 2965 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)) |
158 | | nofun 31802 |
. . . . . . . . . . . 12
⊢ (𝑍 ∈
No → Fun 𝑍) |
159 | | funres 5929 |
. . . . . . . . . . . 12
⊢ (Fun
𝑍 → Fun (𝑍 ↾ dom 𝑈)) |
160 | 131, 158,
159 | 3syl 18 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun (𝑍 ↾ dom 𝑈)) |
161 | 132, 94 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun 𝑈) |
162 | | eqfunfv 6316 |
. . . . . . . . . . 11
⊢ ((Fun
(𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))) |
163 | 160, 161,
162 | syl2anc 693 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))) |
164 | 141, 157,
163 | mpbir2and 957 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ dom 𝑈) = 𝑈) |
165 | 131, 158 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun 𝑍) |
166 | | funfn 5918 |
. . . . . . . . . . . 12
⊢ (Fun
𝑍 ↔ 𝑍 Fn dom 𝑍) |
167 | 165, 166 | sylib 208 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 Fn dom 𝑍) |
168 | | 1on 7567 |
. . . . . . . . . . . . . . . . . . . 20
⊢
1𝑜 ∈ On |
169 | 168 | elexi 3213 |
. . . . . . . . . . . . . . . . . . 19
⊢
1𝑜 ∈ V |
170 | 169 | prid1 4297 |
. . . . . . . . . . . . . . . . . 18
⊢
1𝑜 ∈ {1𝑜,
2𝑜} |
171 | 170 | nosgnn0i 31812 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
≠ 1𝑜 |
172 | 132, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Ord dom 𝑈) |
173 | | ndmfv 6218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅) |
174 | 172, 80, 173 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) = ∅) |
175 | 174 | neeq1d 2853 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) ≠ 1𝑜 ↔ ∅
≠ 1𝑜)) |
176 | 171, 175 | mpbiri 248 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈) ≠
1𝑜) |
177 | 176 | neneqd 2799 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 1𝑜) |
178 | 177 | intnanrd 963 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅)) |
179 | 177 | intnanrd 963 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜)) |
180 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑈 <s 𝑍) |
181 | 132, 131,
55 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈 <s 𝑍 ↔ (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) |
182 | 180, 181 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
183 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈 → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑈‘dom 𝑈)) |
184 | 183 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑈‘dom 𝑈)) |
185 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈 → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘dom 𝑈)) |
186 | 185 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘dom 𝑈)) |
187 | 182, 184,
186 | 3brtr3d 4684 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘dom 𝑈){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝑍‘dom 𝑈)) |
188 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈‘dom 𝑈) ∈ V |
189 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍‘dom 𝑈) ∈ V |
190 | 188, 189 | brtp 31639 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈‘dom 𝑈){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) =
2𝑜))) |
191 | | 3orrot 1044 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜)) ↔ (((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅))) |
192 | | 3orrot 1044 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅)) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) =
2𝑜))) |
193 | 190, 191,
192 | 3bitri 286 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈‘dom 𝑈){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝑍‘dom 𝑈) ↔ (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) =
2𝑜))) |
194 | 187, 193 | sylib 208 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) = ∅) ∨ ((𝑈‘dom 𝑈) = 1𝑜 ∧ (𝑍‘dom 𝑈) =
2𝑜))) |
195 | 178, 179,
194 | ecase23d 1436 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑈‘dom 𝑈) = ∅ ∧ (𝑍‘dom 𝑈) = 2𝑜)) |
196 | 195 | simprd 479 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 2𝑜) |
197 | | ndmfv 6218 |
. . . . . . . . . . . . . 14
⊢ (¬
dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅) |
198 | 105 | nosgnn0i 31812 |
. . . . . . . . . . . . . . . 16
⊢ ∅
≠ 2𝑜 |
199 | | neeq1 2856 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 2𝑜 ↔ ∅
≠ 2𝑜)) |
200 | 198, 199 | mpbiri 248 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠
2𝑜) |
201 | 200 | neneqd 2799 |
. . . . . . . . . . . . . 14
⊢ ((𝑍‘dom 𝑈) = ∅ → ¬ (𝑍‘dom 𝑈) = 2𝑜) |
202 | 197, 201 | syl 17 |
. . . . . . . . . . . . 13
⊢ (¬
dom 𝑈 ∈ dom 𝑍 → ¬ (𝑍‘dom 𝑈) = 2𝑜) |
203 | 202 | con4i 113 |
. . . . . . . . . . . 12
⊢ ((𝑍‘dom 𝑈) = 2𝑜 → dom 𝑈 ∈ dom 𝑍) |
204 | 196, 203 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ∈ dom 𝑍) |
205 | | fnressn 6425 |
. . . . . . . . . . 11
⊢ ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {〈dom 𝑈, (𝑍‘dom 𝑈)〉}) |
206 | 167, 204,
205 | syl2anc 693 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {〈dom 𝑈, (𝑍‘dom 𝑈)〉}) |
207 | 196 | opeq2d 4409 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 〈dom 𝑈, (𝑍‘dom 𝑈)〉 = 〈dom 𝑈,
2𝑜〉) |
208 | 207 | sneqd 4189 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → {〈dom 𝑈, (𝑍‘dom 𝑈)〉} = {〈dom 𝑈,
2𝑜〉}) |
209 | 206, 208 | eqtrd 2656 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {〈dom 𝑈,
2𝑜〉}) |
210 | 164, 209 | uneq12d 3768 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {〈dom 𝑈,
2𝑜〉})) |
211 | 124, 210 | syl5eq 2668 |
. . . . . . 7
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {〈dom 𝑈,
2𝑜〉})) |
212 | | sonr 5056 |
. . . . . . . . 9
⊢ (( <s
Or No ∧ (𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) ∈ No ) → ¬ (𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉})) |
213 | 12, 212 | mpan 706 |
. . . . . . . 8
⊢ ((𝑈 ∪ {〈dom 𝑈, 2𝑜〉})
∈ No → ¬ (𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉})) |
214 | 132, 106,
213 | 3syl 18 |
. . . . . . 7
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {〈dom 𝑈, 2𝑜〉}) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉})) |
215 | 211, 214 | eqnbrtrd 4671 |
. . . . . 6
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉})) |
216 | 120, 215 | jaodan 826 |
. . . . 5
⊢
(((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) ∧ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈)) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉})) |
217 | 216 | ex 450 |
. . . 4
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ((∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉}))) |
218 | 29, 217 | sylbid 230 |
. . 3
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → (∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉}))) |
219 | 23, 218 | mpd 15 |
. 2
⊢ ((((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) ∧ 𝑈 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉})) |
220 | 5, 219 | mpdan 702 |
1
⊢ (((𝑈 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑈 <s 𝑦) ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V ∧
𝑍 ∈ No ) ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈,
2𝑜〉})) |