| Step | Hyp | Ref
| Expression |
| 1 | | breq2 5147 |
. . 3
⊢ (𝑏 = 𝑈 → (𝑍 <s 𝑏 ↔ 𝑍 <s 𝑈)) |
| 2 | | simp3 1139 |
. . 3
⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) |
| 3 | | simp1l 1198 |
. . 3
⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) → 𝑈 ∈ 𝐵) |
| 4 | 1, 2, 3 | rspcdva 3623 |
. 2
⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) → 𝑍 <s 𝑈) |
| 5 | | simpl21 1252 |
. . . . . . . . . . 11
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝐵 ⊆ No
) |
| 6 | | simpl1l 1225 |
. . . . . . . . . . 11
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 ∈ 𝐵) |
| 7 | 5, 6 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 ∈ No
) |
| 8 | | nodmon 27695 |
. . . . . . . . . 10
⊢ (𝑈 ∈
No → dom 𝑈
∈ On) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → dom 𝑈 ∈ On) |
| 10 | | onelon 6409 |
. . . . . . . . 9
⊢ ((dom
𝑈 ∈ On ∧ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On) |
| 11 | 9, 10 | sylan 580 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On) |
| 12 | | simpr 484 |
. . . . . . . . . . . 12
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) |
| 13 | | simplr 769 |
. . . . . . . . . . . 12
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) |
| 14 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → dom 𝑈 ∈ On) |
| 15 | 14 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → dom 𝑈 ∈ On) |
| 16 | | ontr1 6430 |
. . . . . . . . . . . . 13
⊢ (dom
𝑈 ∈ On → ((𝑞 ∈ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . . 12
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈)) |
| 18 | 12, 13, 17 | mp2and 699 |
. . . . . . . . . . 11
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ dom 𝑈) |
| 19 | 18 | fvresd 6926 |
. . . . . . . . . 10
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍‘𝑞)) |
| 20 | | onelon 6409 |
. . . . . . . . . . . . 13
⊢ ((∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ On) |
| 21 | 11, 20 | sylan 580 |
. . . . . . . . . . . 12
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → 𝑞 ∈ On) |
| 22 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑞 → (𝑈‘𝑥) = (𝑈‘𝑞)) |
| 23 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑞 → (𝑍‘𝑥) = (𝑍‘𝑞)) |
| 24 | 22, 23 | neeq12d 3002 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑞 → ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑈‘𝑞) ≠ (𝑍‘𝑞))) |
| 25 | 24 | onnminsb 7819 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ On → (𝑞 ∈ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞))) |
| 26 | 21, 12, 25 | sylc 65 |
. . . . . . . . . . 11
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) |
| 27 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ ((𝑈‘𝑞) ≠ (𝑍‘𝑞) ↔ ¬ (𝑈‘𝑞) = (𝑍‘𝑞)) |
| 28 | 27 | con2bii 357 |
. . . . . . . . . . 11
⊢ ((𝑈‘𝑞) = (𝑍‘𝑞) ↔ ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) |
| 29 | 26, 28 | sylibr 234 |
. . . . . . . . . 10
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → (𝑈‘𝑞) = (𝑍‘𝑞)) |
| 30 | 19, 29 | eqtr4d 2780 |
. . . . . . . . 9
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) ∧ 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)) |
| 31 | 30 | ralrimiva 3146 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)) |
| 32 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) |
| 33 | 32 | fvresd 6926 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
| 34 | | simplr 769 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑍 <s 𝑈) |
| 35 | | simpl23 1254 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 ∈ No
) |
| 36 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → 𝑈 ∈ No
) |
| 37 | | sltval2 27701 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈
No ∧ 𝑈 ∈
No ) → (𝑍 <s 𝑈 ↔ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}))) |
| 38 | 35, 36, 37 | syl2an2r 685 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}))) |
| 39 | 34, 38 | mpbid 232 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})) |
| 40 | | necom 2994 |
. . . . . . . . . . . . 13
⊢ ((𝑈‘𝑥) ≠ (𝑍‘𝑥) ↔ (𝑍‘𝑥) ≠ (𝑈‘𝑥)) |
| 41 | 40 | rabbii 3442 |
. . . . . . . . . . . 12
⊢ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} |
| 42 | 41 | inteqi 4950 |
. . . . . . . . . . 11
⊢ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} |
| 43 | 42 | fveq2i 6909 |
. . . . . . . . . 10
⊢ (𝑍‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}) |
| 44 | 42 | fveq2i 6909 |
. . . . . . . . . 10
⊢ (𝑈‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) = (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}) |
| 45 | 39, 43, 44 | 3brtr4g 5177 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
| 46 | 33, 45 | eqbrtrd 5165 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
| 47 | | raleq 3323 |
. . . . . . . . . 10
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ↔ ∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))) |
| 48 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((𝑍 ↾ dom 𝑈)‘𝑝) = ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
| 49 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (𝑈‘𝑝) = (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})) |
| 50 | 48, 49 | breq12d 5156 |
. . . . . . . . . 10
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → (((𝑍 ↾ dom 𝑈)‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘𝑝) ↔ ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) |
| 51 | 47, 50 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑝 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} → ((∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘𝑝)) ↔ (∀𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)})))) |
| 52 | 51 | rspcev 3622 |
. . . . . . . 8
⊢ ((∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ (∀𝑞 ∈ ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}))) → ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘𝑝))) |
| 53 | 11, 31, 46, 52 | syl12anc 837 |
. . . . . . 7
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘𝑝))) |
| 54 | | noreson 27705 |
. . . . . . . . 9
⊢ ((𝑍 ∈
No ∧ dom 𝑈
∈ On) → (𝑍
↾ dom 𝑈) ∈ No ) |
| 55 | 35, 9, 54 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ dom 𝑈) ∈ No
) |
| 56 | | sltval 27692 |
. . . . . . . 8
⊢ (((𝑍 ↾ dom 𝑈) ∈ No
∧ 𝑈 ∈ No ) → ((𝑍 ↾ dom 𝑈) <s 𝑈 ↔ ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘𝑝)))) |
| 57 | 55, 36, 56 | syl2an2r 685 |
. . . . . . 7
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈) <s 𝑈 ↔ ∃𝑝 ∈ On (∀𝑞 ∈ 𝑝 ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞) ∧ ((𝑍 ↾ dom 𝑈)‘𝑝){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘𝑝)))) |
| 58 | 53, 57 | mpbird 257 |
. . . . . 6
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ dom 𝑈) <s 𝑈) |
| 59 | | sssucid 6464 |
. . . . . . 7
⊢ dom 𝑈 ⊆ suc dom 𝑈 |
| 60 | | resabs1 6024 |
. . . . . . 7
⊢ (dom
𝑈 ⊆ suc dom 𝑈 → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈)) |
| 61 | 59, 60 | mp1i 13 |
. . . . . 6
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) = (𝑍 ↾ dom 𝑈)) |
| 62 | | resundir 6012 |
. . . . . . 7
⊢ ((𝑈 ∪ {〈dom 𝑈, 1o〉}) ↾
dom 𝑈) = ((𝑈 ↾ dom 𝑈) ∪ ({〈dom 𝑈, 1o〉} ↾ dom 𝑈)) |
| 63 | | nofun 27694 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈
No → Fun 𝑈) |
| 64 | 7, 63 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑈) |
| 65 | | funrel 6583 |
. . . . . . . . . . . 12
⊢ (Fun
𝑈 → Rel 𝑈) |
| 66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Rel 𝑈) |
| 67 | 66 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → Rel 𝑈) |
| 68 | | resdm 6044 |
. . . . . . . . . 10
⊢ (Rel
𝑈 → (𝑈 ↾ dom 𝑈) = 𝑈) |
| 69 | 67, 68 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ↾ dom 𝑈) = 𝑈) |
| 70 | | nodmord 27698 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈
No → Ord dom 𝑈) |
| 71 | 7, 70 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Ord dom 𝑈) |
| 72 | 71 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → Ord dom 𝑈) |
| 73 | | ordirr 6402 |
. . . . . . . . . . 11
⊢ (Ord dom
𝑈 → ¬ dom 𝑈 ∈ dom 𝑈) |
| 74 | 72, 73 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ¬ dom 𝑈 ∈ dom 𝑈) |
| 75 | | 1oex 8516 |
. . . . . . . . . . 11
⊢
1o ∈ V |
| 76 | 75 | snres0 6318 |
. . . . . . . . . 10
⊢
(({〈dom 𝑈,
1o〉} ↾ dom 𝑈) = ∅ ↔ ¬ dom 𝑈 ∈ dom 𝑈) |
| 77 | 74, 76 | sylibr 234 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ({〈dom 𝑈, 1o〉} ↾ dom 𝑈) = ∅) |
| 78 | 69, 77 | uneq12d 4169 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({〈dom 𝑈, 1o〉} ↾ dom 𝑈)) = (𝑈 ∪ ∅)) |
| 79 | | un0 4394 |
. . . . . . . 8
⊢ (𝑈 ∪ ∅) = 𝑈 |
| 80 | 78, 79 | eqtrdi 2793 |
. . . . . . 7
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ↾ dom 𝑈) ∪ ({〈dom 𝑈, 1o〉} ↾ dom 𝑈)) = 𝑈) |
| 81 | 62, 80 | eqtrid 2789 |
. . . . . 6
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑈 ∪ {〈dom 𝑈, 1o〉}) ↾ dom 𝑈) = 𝑈) |
| 82 | 58, 61, 81 | 3brtr4d 5175 |
. . . . 5
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {〈dom 𝑈, 1o〉}) ↾ dom 𝑈)) |
| 83 | | onsucb 7837 |
. . . . . . . . 9
⊢ (dom
𝑈 ∈ On ↔ suc dom
𝑈 ∈
On) |
| 84 | 9, 83 | sylib 218 |
. . . . . . . 8
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → suc dom 𝑈 ∈ On) |
| 85 | | noreson 27705 |
. . . . . . . 8
⊢ ((𝑍 ∈
No ∧ suc dom 𝑈
∈ On) → (𝑍
↾ suc dom 𝑈) ∈
No ) |
| 86 | 35, 84, 85 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No
) |
| 87 | 86 | adantr 480 |
. . . . . 6
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) ∈ No
) |
| 88 | 75 | prid1 4762 |
. . . . . . . . 9
⊢
1o ∈ {1o, 2o} |
| 89 | 88 | noextend 27711 |
. . . . . . . 8
⊢ (𝑈 ∈
No → (𝑈 ∪
{〈dom 𝑈,
1o〉}) ∈ No
) |
| 90 | 7, 89 | syl 17 |
. . . . . . 7
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑈 ∪ {〈dom 𝑈, 1o〉}) ∈ No ) |
| 91 | 90 | adantr 480 |
. . . . . 6
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑈 ∪ {〈dom 𝑈, 1o〉}) ∈ No ) |
| 92 | | sltres 27707 |
. . . . . 6
⊢ (((𝑍 ↾ suc dom 𝑈) ∈
No ∧ (𝑈 ∪
{〈dom 𝑈,
1o〉}) ∈ No ∧ dom 𝑈 ∈ On) → (((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {〈dom 𝑈, 1o〉}) ↾ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 1o〉}))) |
| 93 | 87, 91, 14, 92 | syl3anc 1373 |
. . . . 5
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (((𝑍 ↾ suc dom 𝑈) ↾ dom 𝑈) <s ((𝑈 ∪ {〈dom 𝑈, 1o〉}) ↾ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 1o〉}))) |
| 94 | 82, 93 | mpd 15 |
. . . 4
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → (𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 1o〉})) |
| 95 | | sltso 27721 |
. . . . . 6
⊢ <s Or
No |
| 96 | | soasym 5625 |
. . . . . 6
⊢ (( <s
Or No ∧ ((𝑍 ↾ suc dom 𝑈) ∈ No
∧ (𝑈 ∪ {〈dom
𝑈, 1o〉})
∈ No )) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 1o〉}) → ¬ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s
(𝑍 ↾ suc dom 𝑈))) |
| 97 | 95, 96 | mpan 690 |
. . . . 5
⊢ (((𝑍 ↾ suc dom 𝑈) ∈
No ∧ (𝑈 ∪
{〈dom 𝑈,
1o〉}) ∈ No ) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 1o〉}) → ¬ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s
(𝑍 ↾ suc dom 𝑈))) |
| 98 | 86, 91, 97 | syl2an2r 685 |
. . . 4
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ((𝑍 ↾ suc dom 𝑈) <s (𝑈 ∪ {〈dom 𝑈, 1o〉}) → ¬ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s
(𝑍 ↾ suc dom 𝑈))) |
| 99 | 94, 98 | mpd 15 |
. . 3
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈) → ¬ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s (𝑍 ↾ suc dom 𝑈)) |
| 100 | | sonr 5616 |
. . . . . 6
⊢ (( <s
Or No ∧ (𝑈 ∪ {〈dom 𝑈, 1o〉}) ∈ No ) → ¬ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s (𝑈 ∪ {〈dom 𝑈,
1o〉})) |
| 101 | 95, 90, 100 | sylancr 587 |
. . . . 5
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s (𝑈 ∪ {〈dom 𝑈,
1o〉})) |
| 102 | 101 | adantr 480 |
. . . 4
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s (𝑈 ∪ {〈dom 𝑈,
1o〉})) |
| 103 | | df-suc 6390 |
. . . . . . . 8
⊢ suc dom
𝑈 = (dom 𝑈 ∪ {dom 𝑈}) |
| 104 | 103 | reseq2i 5994 |
. . . . . . 7
⊢ (𝑍 ↾ suc dom 𝑈) = (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) |
| 105 | | resundi 6011 |
. . . . . . 7
⊢ (𝑍 ↾ (dom 𝑈 ∪ {dom 𝑈})) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) |
| 106 | 104, 105 | eqtri 2765 |
. . . . . 6
⊢ (𝑍 ↾ suc dom 𝑈) = ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) |
| 107 | | dmres 6030 |
. . . . . . . . 9
⊢ dom
(𝑍 ↾ dom 𝑈) = (dom 𝑈 ∩ dom 𝑍) |
| 108 | 42 | eqeq1i 2742 |
. . . . . . . . . . . . 13
⊢ (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈 ↔ ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} = dom 𝑈) |
| 109 | 108 | biimpi 216 |
. . . . . . . . . . . 12
⊢ (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈 → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} = dom 𝑈) |
| 110 | 109 | adantl 481 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} = dom 𝑈) |
| 111 | 35 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 ∈ No
) |
| 112 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑈 ∈ No
) |
| 113 | | simp23 1209 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) → 𝑍 ∈ No
) |
| 114 | | sonr 5616 |
. . . . . . . . . . . . . . . . . 18
⊢ (( <s
Or No ∧ 𝑍 ∈ No )
→ ¬ 𝑍 <s 𝑍) |
| 115 | 95, 113, 114 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) → ¬ 𝑍 <s 𝑍) |
| 116 | | breq2 5147 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 = 𝑍 → (𝑍 <s 𝑈 ↔ 𝑍 <s 𝑍)) |
| 117 | 116 | notbid 318 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 = 𝑍 → (¬ 𝑍 <s 𝑈 ↔ ¬ 𝑍 <s 𝑍)) |
| 118 | 115, 117 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) → (𝑈 = 𝑍 → ¬ 𝑍 <s 𝑈)) |
| 119 | 118 | necon2ad 2955 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) → (𝑍 <s 𝑈 → 𝑈 ≠ 𝑍)) |
| 120 | 119 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑈 ≠ 𝑍) |
| 121 | 120 | necomd 2996 |
. . . . . . . . . . . . 13
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 ≠ 𝑈) |
| 122 | 121 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 𝑍 ≠ 𝑈) |
| 123 | | nosepssdm 27731 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈
No ∧ 𝑈 ∈
No ∧ 𝑍 ≠ 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} ⊆ dom 𝑍) |
| 124 | 111, 112,
122, 123 | syl3anc 1373 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)} ⊆ dom 𝑍) |
| 125 | 110, 124 | eqsstrrd 4019 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ⊆ dom 𝑍) |
| 126 | | dfss2 3969 |
. . . . . . . . . 10
⊢ (dom
𝑈 ⊆ dom 𝑍 ↔ (dom 𝑈 ∩ dom 𝑍) = dom 𝑈) |
| 127 | 125, 126 | sylib 218 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (dom 𝑈 ∩ dom 𝑍) = dom 𝑈) |
| 128 | 107, 127 | eqtrid 2789 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom (𝑍 ↾ dom 𝑈) = dom 𝑈) |
| 129 | 128 | eleq2d 2827 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) ↔ 𝑞 ∈ dom 𝑈)) |
| 130 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ dom 𝑈) |
| 131 | 130 | fvresd 6926 |
. . . . . . . . . . . 12
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑍‘𝑞)) |
| 132 | 112, 8 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ∈ On) |
| 133 | | onelon 6409 |
. . . . . . . . . . . . . . 15
⊢ ((dom
𝑈 ∈ On ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On) |
| 134 | 132, 133 | sylan 580 |
. . . . . . . . . . . . . 14
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ On) |
| 135 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) |
| 136 | 135 | eleq2d 2827 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ↔ 𝑞 ∈ dom 𝑈)) |
| 137 | 136 | biimpar 477 |
. . . . . . . . . . . . . 14
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → 𝑞 ∈ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)}) |
| 138 | 134, 137,
25 | sylc 65 |
. . . . . . . . . . . . 13
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) |
| 139 | | nesym 2997 |
. . . . . . . . . . . . . 14
⊢ ((𝑈‘𝑞) ≠ (𝑍‘𝑞) ↔ ¬ (𝑍‘𝑞) = (𝑈‘𝑞)) |
| 140 | 139 | con2bii 357 |
. . . . . . . . . . . . 13
⊢ ((𝑍‘𝑞) = (𝑈‘𝑞) ↔ ¬ (𝑈‘𝑞) ≠ (𝑍‘𝑞)) |
| 141 | 138, 140 | sylibr 234 |
. . . . . . . . . . . 12
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → (𝑍‘𝑞) = (𝑈‘𝑞)) |
| 142 | 131, 141 | eqtrd 2777 |
. . . . . . . . . . 11
⊢
((((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) ∧ 𝑞 ∈ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)) |
| 143 | 142 | ex 412 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom 𝑈 → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))) |
| 144 | 129, 143 | sylbid 240 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑞 ∈ dom (𝑍 ↾ dom 𝑈) → ((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞))) |
| 145 | 144 | ralrimiv 3145 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)) |
| 146 | | nofun 27694 |
. . . . . . . . . . 11
⊢ (𝑍 ∈
No → Fun 𝑍) |
| 147 | 111, 146 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun 𝑍) |
| 148 | 147 | funresd 6609 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun (𝑍 ↾ dom 𝑈)) |
| 149 | 64 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → Fun 𝑈) |
| 150 | | eqfunfv 7056 |
. . . . . . . . 9
⊢ ((Fun
(𝑍 ↾ dom 𝑈) ∧ Fun 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))) |
| 151 | 148, 149,
150 | syl2anc 584 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) = 𝑈 ↔ (dom (𝑍 ↾ dom 𝑈) = dom 𝑈 ∧ ∀𝑞 ∈ dom (𝑍 ↾ dom 𝑈)((𝑍 ↾ dom 𝑈)‘𝑞) = (𝑈‘𝑞)))) |
| 152 | 128, 145,
151 | mpbir2and 713 |
. . . . . . 7
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ dom 𝑈) = 𝑈) |
| 153 | 35, 146 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → Fun 𝑍) |
| 154 | 153 | funfnd 6597 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 Fn dom 𝑍) |
| 155 | | ndmfv 6941 |
. . . . . . . . . . . . . . . 16
⊢ (¬
dom 𝑈 ∈ dom 𝑈 → (𝑈‘dom 𝑈) = ∅) |
| 156 | | 2on0 8522 |
. . . . . . . . . . . . . . . . . . 19
⊢
2o ≠ ∅ |
| 157 | 156 | necomi 2995 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
≠ 2o |
| 158 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈‘dom 𝑈) = ∅ → ((𝑈‘dom 𝑈) ≠ 2o ↔ ∅ ≠
2o)) |
| 159 | 157, 158 | mpbiri 258 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈‘dom 𝑈) = ∅ → (𝑈‘dom 𝑈) ≠ 2o) |
| 160 | 159 | neneqd 2945 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈‘dom 𝑈) = ∅ → ¬ (𝑈‘dom 𝑈) = 2o) |
| 161 | 155, 160 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (¬
dom 𝑈 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑈) = 2o) |
| 162 | 112, 70, 73, 161 | 4syl 19 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈‘dom 𝑈) = 2o) |
| 163 | 162 | intnand 488 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o)) |
| 164 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → 𝑍 <s 𝑈) |
| 165 | 35, 7, 37 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍 <s 𝑈 ↔ (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}))) |
| 166 | 164, 165 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})) |
| 167 | 166 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘∩ {𝑥
∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)})) |
| 168 | 110 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}) = (𝑍‘dom 𝑈)) |
| 169 | 110 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑍‘𝑥) ≠ (𝑈‘𝑥)}) = (𝑈‘dom 𝑈)) |
| 170 | 167, 168,
169 | 3brtr3d 5174 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘dom 𝑈)) |
| 171 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢ (𝑍‘dom 𝑈) ∈ V |
| 172 | | fvex 6919 |
. . . . . . . . . . . . . . 15
⊢ (𝑈‘dom 𝑈) ∈ V |
| 173 | 171, 172 | brtp 5528 |
. . . . . . . . . . . . . 14
⊢ ((𝑍‘dom 𝑈){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝑈‘dom 𝑈) ↔ (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o))) |
| 174 | 170, 173 | sylib 218 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o))) |
| 175 | | 3orel3 1488 |
. . . . . . . . . . . . 13
⊢ (¬
((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o) → ((((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o) ∨ ((𝑍‘dom 𝑈) = ∅ ∧ (𝑈‘dom 𝑈) = 2o)) → (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o)))) |
| 176 | 163, 174,
175 | sylc 65 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o))) |
| 177 | | andi 1010 |
. . . . . . . . . . . 12
⊢ (((𝑍‘dom 𝑈) = 1o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2o)) ↔ (((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = ∅) ∨ ((𝑍‘dom 𝑈) = 1o ∧ (𝑈‘dom 𝑈) = 2o))) |
| 178 | 176, 177 | sylibr 234 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍‘dom 𝑈) = 1o ∧ ((𝑈‘dom 𝑈) = ∅ ∨ (𝑈‘dom 𝑈) = 2o))) |
| 179 | 178 | simpld 494 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍‘dom 𝑈) = 1o) |
| 180 | | ndmfv 6941 |
. . . . . . . . . . . 12
⊢ (¬
dom 𝑈 ∈ dom 𝑍 → (𝑍‘dom 𝑈) = ∅) |
| 181 | | 1n0 8526 |
. . . . . . . . . . . . . . 15
⊢
1o ≠ ∅ |
| 182 | 181 | necomi 2995 |
. . . . . . . . . . . . . 14
⊢ ∅
≠ 1o |
| 183 | | neeq1 3003 |
. . . . . . . . . . . . . 14
⊢ ((𝑍‘dom 𝑈) = ∅ → ((𝑍‘dom 𝑈) ≠ 1o ↔ ∅ ≠
1o)) |
| 184 | 182, 183 | mpbiri 258 |
. . . . . . . . . . . . 13
⊢ ((𝑍‘dom 𝑈) = ∅ → (𝑍‘dom 𝑈) ≠ 1o) |
| 185 | 184 | neneqd 2945 |
. . . . . . . . . . . 12
⊢ ((𝑍‘dom 𝑈) = ∅ → ¬ (𝑍‘dom 𝑈) = 1o) |
| 186 | 180, 185 | syl 17 |
. . . . . . . . . . 11
⊢ (¬
dom 𝑈 ∈ dom 𝑍 → ¬ (𝑍‘dom 𝑈) = 1o) |
| 187 | 186 | con4i 114 |
. . . . . . . . . 10
⊢ ((𝑍‘dom 𝑈) = 1o → dom 𝑈 ∈ dom 𝑍) |
| 188 | 179, 187 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → dom 𝑈 ∈ dom 𝑍) |
| 189 | | fnressn 7178 |
. . . . . . . . 9
⊢ ((𝑍 Fn dom 𝑍 ∧ dom 𝑈 ∈ dom 𝑍) → (𝑍 ↾ {dom 𝑈}) = {〈dom 𝑈, (𝑍‘dom 𝑈)〉}) |
| 190 | 154, 188,
189 | syl2an2r 685 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {〈dom 𝑈, (𝑍‘dom 𝑈)〉}) |
| 191 | 179 | opeq2d 4880 |
. . . . . . . . 9
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → 〈dom 𝑈, (𝑍‘dom 𝑈)〉 = 〈dom 𝑈, 1o〉) |
| 192 | 191 | sneqd 4638 |
. . . . . . . 8
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → {〈dom 𝑈, (𝑍‘dom 𝑈)〉} = {〈dom 𝑈, 1o〉}) |
| 193 | 190, 192 | eqtrd 2777 |
. . . . . . 7
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ {dom 𝑈}) = {〈dom 𝑈, 1o〉}) |
| 194 | 152, 193 | uneq12d 4169 |
. . . . . 6
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑍 ↾ dom 𝑈) ∪ (𝑍 ↾ {dom 𝑈})) = (𝑈 ∪ {〈dom 𝑈, 1o〉})) |
| 195 | 106, 194 | eqtrid 2789 |
. . . . 5
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → (𝑍 ↾ suc dom 𝑈) = (𝑈 ∪ {〈dom 𝑈, 1o〉})) |
| 196 | 195 | breq2d 5155 |
. . . 4
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ((𝑈 ∪ {〈dom 𝑈, 1o〉}) <s (𝑍 ↾ suc dom 𝑈) ↔ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s (𝑈 ∪ {〈dom 𝑈,
1o〉}))) |
| 197 | 102, 196 | mtbird 325 |
. . 3
⊢
(((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) ∧ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈) → ¬ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s (𝑍 ↾ suc dom 𝑈)) |
| 198 | | nosepssdm 27731 |
. . . . 5
⊢ ((𝑈 ∈
No ∧ 𝑍 ∈
No ∧ 𝑈 ≠ 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈) |
| 199 | 7, 35, 120, 198 | syl3anc 1373 |
. . . 4
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈) |
| 200 | | nosepon 27710 |
. . . . . 6
⊢ ((𝑈 ∈
No ∧ 𝑍 ∈
No ∧ 𝑈 ≠ 𝑍) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On) |
| 201 | 7, 35, 120, 200 | syl3anc 1373 |
. . . . 5
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On) |
| 202 | | onsseleq 6425 |
. . . . 5
⊢ ((∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ On ∧ dom 𝑈 ∈ On) → (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 ↔ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈))) |
| 203 | 201, 9, 202 | syl2anc 584 |
. . . 4
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ⊆ dom 𝑈 ↔ (∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈))) |
| 204 | 199, 203 | mpbid 232 |
. . 3
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → (∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} ∈ dom 𝑈 ∨ ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑍‘𝑥)} = dom 𝑈)) |
| 205 | 99, 197, 204 | mpjaodan 961 |
. 2
⊢ ((((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) ∧ 𝑍 <s 𝑈) → ¬ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s (𝑍 ↾ suc dom 𝑈)) |
| 206 | 4, 205 | mpdan 687 |
1
⊢ (((𝑈 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑈) ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No )
∧ ∀𝑏 ∈
𝐵 𝑍 <s 𝑏) → ¬ (𝑈 ∪ {〈dom 𝑈, 1o〉}) <s (𝑍 ↾ suc dom 𝑈)) |