Step | Hyp | Ref
| Expression |
1 | | nofun 27020 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → Fun 𝐴) |
2 | | funfn 6535 |
. . . . . . . . 9
⊢ (Fun
𝐴 ↔ 𝐴 Fn dom 𝐴) |
3 | 1, 2 | sylib 217 |
. . . . . . . 8
⊢ (𝐴 ∈
No → 𝐴 Fn dom
𝐴) |
4 | | nodmon 27021 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → dom 𝐴
∈ On) |
5 | | 1on 8428 |
. . . . . . . . 9
⊢
1o ∈ On |
6 | | fnsng 6557 |
. . . . . . . . 9
⊢ ((dom
𝐴 ∈ On ∧
1o ∈ On) → {⟨dom 𝐴, 1o⟩} Fn {dom 𝐴}) |
7 | 4, 5, 6 | sylancl 587 |
. . . . . . . 8
⊢ (𝐴 ∈
No → {⟨dom 𝐴, 1o⟩} Fn {dom 𝐴}) |
8 | | nodmord 27024 |
. . . . . . . . . 10
⊢ (𝐴 ∈
No → Ord dom 𝐴) |
9 | | ordirr 6339 |
. . . . . . . . . 10
⊢ (Ord dom
𝐴 → ¬ dom 𝐴 ∈ dom 𝐴) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → ¬ dom 𝐴 ∈ dom 𝐴) |
11 | | disjsn 4676 |
. . . . . . . . 9
⊢ ((dom
𝐴 ∩ {dom 𝐴}) = ∅ ↔ ¬ dom
𝐴 ∈ dom 𝐴) |
12 | 10, 11 | sylibr 233 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (dom 𝐴
∩ {dom 𝐴}) =
∅) |
13 | | snidg 4624 |
. . . . . . . . 9
⊢ (dom
𝐴 ∈ On → dom
𝐴 ∈ {dom 𝐴}) |
14 | 4, 13 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈
No → dom 𝐴
∈ {dom 𝐴}) |
15 | | fvun2 6937 |
. . . . . . . 8
⊢ ((𝐴 Fn dom 𝐴 ∧ {⟨dom 𝐴, 1o⟩} Fn {dom 𝐴} ∧ ((dom 𝐴 ∩ {dom 𝐴}) = ∅ ∧ dom 𝐴 ∈ {dom 𝐴})) → ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘dom 𝐴) = ({⟨dom 𝐴, 1o⟩}‘dom
𝐴)) |
16 | 3, 7, 12, 14, 15 | syl112anc 1375 |
. . . . . . 7
⊢ (𝐴 ∈
No → ((𝐴 ∪
{⟨dom 𝐴,
1o⟩})‘dom 𝐴) = ({⟨dom 𝐴, 1o⟩}‘dom 𝐴)) |
17 | | fvsng 7130 |
. . . . . . . 8
⊢ ((dom
𝐴 ∈ On ∧
1o ∈ On) → ({⟨dom 𝐴, 1o⟩}‘dom 𝐴) =
1o) |
18 | 4, 5, 17 | sylancl 587 |
. . . . . . 7
⊢ (𝐴 ∈
No → ({⟨dom 𝐴, 1o⟩}‘dom 𝐴) =
1o) |
19 | 16, 18 | eqtrd 2773 |
. . . . . 6
⊢ (𝐴 ∈
No → ((𝐴 ∪
{⟨dom 𝐴,
1o⟩})‘dom 𝐴) = 1o) |
20 | | ndmfv 6881 |
. . . . . . 7
⊢ (¬
dom 𝐴 ∈ dom 𝐴 → (𝐴‘dom 𝐴) = ∅) |
21 | 10, 20 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈
No → (𝐴‘dom 𝐴) = ∅) |
22 | 19, 21 | jca 513 |
. . . . 5
⊢ (𝐴 ∈
No → (((𝐴
∪ {⟨dom 𝐴,
1o⟩})‘dom 𝐴) = 1o ∧ (𝐴‘dom 𝐴) = ∅)) |
23 | 22 | 3mix1d 1337 |
. . . 4
⊢ (𝐴 ∈
No → ((((𝐴
∪ {⟨dom 𝐴,
1o⟩})‘dom 𝐴) = 1o ∧ (𝐴‘dom 𝐴) = ∅) ∨ (((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘dom 𝐴) = 1o ∧ (𝐴‘dom 𝐴) = 2o) ∨ (((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘dom 𝐴) = ∅ ∧ (𝐴‘dom 𝐴) = 2o))) |
24 | | fvex 6859 |
. . . . 5
⊢ ((𝐴 ∪ {⟨dom 𝐴,
1o⟩})‘dom 𝐴) ∈ V |
25 | | fvex 6859 |
. . . . 5
⊢ (𝐴‘dom 𝐴) ∈ V |
26 | 24, 25 | brtp 5484 |
. . . 4
⊢ (((𝐴 ∪ {⟨dom 𝐴,
1o⟩})‘dom 𝐴){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝐴‘dom 𝐴) ↔ ((((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘dom 𝐴) = 1o ∧ (𝐴‘dom 𝐴) = ∅) ∨ (((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘dom 𝐴) = 1o ∧ (𝐴‘dom 𝐴) = 2o) ∨ (((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘dom 𝐴) = ∅ ∧ (𝐴‘dom 𝐴) = 2o))) |
27 | 23, 26 | sylibr 233 |
. . 3
⊢ (𝐴 ∈
No → ((𝐴 ∪
{⟨dom 𝐴,
1o⟩})‘dom 𝐴){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝐴‘dom 𝐴)) |
28 | | necom 2994 |
. . . . . . 7
⊢ (((𝐴 ∪ {⟨dom 𝐴,
1o⟩})‘𝑥) ≠ (𝐴‘𝑥) ↔ (𝐴‘𝑥) ≠ ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘𝑥)) |
29 | 28 | rabbii 3412 |
. . . . . 6
⊢ {𝑥 ∈ On ∣ ((𝐴 ∪ {⟨dom 𝐴,
1o⟩})‘𝑥) ≠ (𝐴‘𝑥)} = {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘𝑥)} |
30 | 29 | inteqi 4915 |
. . . . 5
⊢ ∩ {𝑥
∈ On ∣ ((𝐴 ∪
{⟨dom 𝐴,
1o⟩})‘𝑥) ≠ (𝐴‘𝑥)} = ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘𝑥)} |
31 | | 1oex 8426 |
. . . . . . 7
⊢
1o ∈ V |
32 | 31 | prid1 4727 |
. . . . . 6
⊢
1o ∈ {1o, 2o} |
33 | 32 | noextenddif 27039 |
. . . . 5
⊢ (𝐴 ∈
No → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘𝑥)} = dom 𝐴) |
34 | 30, 33 | eqtrid 2785 |
. . . 4
⊢ (𝐴 ∈
No → ∩ {𝑥 ∈ On ∣ ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘𝑥) ≠ (𝐴‘𝑥)} = dom 𝐴) |
35 | 34 | fveq2d 6850 |
. . 3
⊢ (𝐴 ∈
No → ((𝐴 ∪
{⟨dom 𝐴,
1o⟩})‘∩ {𝑥 ∈ On ∣ ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘𝑥) ≠ (𝐴‘𝑥)}) = ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘dom 𝐴)) |
36 | 34 | fveq2d 6850 |
. . 3
⊢ (𝐴 ∈
No → (𝐴‘∩ {𝑥 ∈ On ∣ ((𝐴 ∪ {⟨dom 𝐴,
1o⟩})‘𝑥) ≠ (𝐴‘𝑥)}) = (𝐴‘dom 𝐴)) |
37 | 27, 35, 36 | 3brtr4d 5141 |
. 2
⊢ (𝐴 ∈
No → ((𝐴 ∪
{⟨dom 𝐴,
1o⟩})‘∩ {𝑥 ∈ On ∣ ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘𝑥) ≠ (𝐴‘𝑥)}){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝐴‘∩ {𝑥
∈ On ∣ ((𝐴 ∪
{⟨dom 𝐴,
1o⟩})‘𝑥) ≠ (𝐴‘𝑥)})) |
38 | 32 | noextend 27037 |
. . 3
⊢ (𝐴 ∈
No → (𝐴 ∪
{⟨dom 𝐴,
1o⟩}) ∈ No
) |
39 | | sltval2 27027 |
. . 3
⊢ (((𝐴 ∪ {⟨dom 𝐴, 1o⟩}) ∈
No ∧ 𝐴 ∈ No )
→ ((𝐴 ∪ {⟨dom
𝐴, 1o⟩})
<s 𝐴 ↔ ((𝐴 ∪ {⟨dom 𝐴,
1o⟩})‘∩ {𝑥 ∈ On ∣ ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘𝑥) ≠ (𝐴‘𝑥)}){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝐴‘∩ {𝑥
∈ On ∣ ((𝐴 ∪
{⟨dom 𝐴,
1o⟩})‘𝑥) ≠ (𝐴‘𝑥)}))) |
40 | 38, 39 | mpancom 687 |
. 2
⊢ (𝐴 ∈
No → ((𝐴 ∪
{⟨dom 𝐴,
1o⟩}) <s 𝐴 ↔ ((𝐴 ∪ {⟨dom 𝐴, 1o⟩})‘∩ {𝑥
∈ On ∣ ((𝐴 ∪
{⟨dom 𝐴,
1o⟩})‘𝑥) ≠ (𝐴‘𝑥)}){⟨1o, ∅⟩,
⟨1o, 2o⟩, ⟨∅, 2o⟩}
(𝐴‘∩ {𝑥
∈ On ∣ ((𝐴 ∪
{⟨dom 𝐴,
1o⟩})‘𝑥) ≠ (𝐴‘𝑥)}))) |
41 | 37, 40 | mpbird 257 |
1
⊢ (𝐴 ∈
No → (𝐴 ∪
{⟨dom 𝐴,
1o⟩}) <s 𝐴) |