Step | Hyp | Ref
| Expression |
1 | | nodmord 33850 |
. . . . . . . 8
⊢ (𝐴 ∈
No → Ord dom 𝐴) |
2 | | ordirr 6282 |
. . . . . . . 8
⊢ (Ord dom
𝐴 → ¬ dom 𝐴 ∈ dom 𝐴) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈
No → ¬ dom 𝐴 ∈ dom 𝐴) |
4 | | ndmfv 6799 |
. . . . . . 7
⊢ (¬
dom 𝐴 ∈ dom 𝐴 → (𝐴‘dom 𝐴) = ∅) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈
No → (𝐴‘dom 𝐴) = ∅) |
6 | | nofun 33846 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → Fun 𝐴) |
7 | | funfn 6461 |
. . . . . . . . 9
⊢ (Fun
𝐴 ↔ 𝐴 Fn dom 𝐴) |
8 | 6, 7 | sylib 217 |
. . . . . . . 8
⊢ (𝐴 ∈
No → 𝐴 Fn dom
𝐴) |
9 | | nodmon 33847 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → dom 𝐴
∈ On) |
10 | | 2on 8300 |
. . . . . . . . 9
⊢
2o ∈ On |
11 | | fnsng 6483 |
. . . . . . . . 9
⊢ ((dom
𝐴 ∈ On ∧
2o ∈ On) → {〈dom 𝐴, 2o〉} Fn {dom 𝐴}) |
12 | 9, 10, 11 | sylancl 586 |
. . . . . . . 8
⊢ (𝐴 ∈
No → {〈dom 𝐴, 2o〉} Fn {dom 𝐴}) |
13 | | disjsn 4653 |
. . . . . . . . 9
⊢ ((dom
𝐴 ∩ {dom 𝐴}) = ∅ ↔ ¬ dom
𝐴 ∈ dom 𝐴) |
14 | 3, 13 | sylibr 233 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (dom 𝐴
∩ {dom 𝐴}) =
∅) |
15 | | snidg 4601 |
. . . . . . . . 9
⊢ (dom
𝐴 ∈ On → dom
𝐴 ∈ {dom 𝐴}) |
16 | 9, 15 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈
No → dom 𝐴
∈ {dom 𝐴}) |
17 | | fvun2 6855 |
. . . . . . . 8
⊢ ((𝐴 Fn dom 𝐴 ∧ {〈dom 𝐴, 2o〉} Fn {dom 𝐴} ∧ ((dom 𝐴 ∩ {dom 𝐴}) = ∅ ∧ dom 𝐴 ∈ {dom 𝐴})) → ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) = ({〈dom 𝐴, 2o〉}‘dom
𝐴)) |
18 | 8, 12, 14, 16, 17 | syl112anc 1373 |
. . . . . . 7
⊢ (𝐴 ∈
No → ((𝐴 ∪
{〈dom 𝐴,
2o〉})‘dom 𝐴) = ({〈dom 𝐴, 2o〉}‘dom 𝐴)) |
19 | | fvsng 7047 |
. . . . . . . 8
⊢ ((dom
𝐴 ∈ On ∧
2o ∈ On) → ({〈dom 𝐴, 2o〉}‘dom 𝐴) =
2o) |
20 | 9, 10, 19 | sylancl 586 |
. . . . . . 7
⊢ (𝐴 ∈
No → ({〈dom 𝐴, 2o〉}‘dom 𝐴) =
2o) |
21 | 18, 20 | eqtrd 2780 |
. . . . . 6
⊢ (𝐴 ∈
No → ((𝐴 ∪
{〈dom 𝐴,
2o〉})‘dom 𝐴) = 2o) |
22 | 5, 21 | jca 512 |
. . . . 5
⊢ (𝐴 ∈
No → ((𝐴‘dom 𝐴) = ∅ ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) =
2o)) |
23 | 22 | 3mix3d 1337 |
. . . 4
⊢ (𝐴 ∈
No → (((𝐴‘dom 𝐴) = 1o ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) = ∅) ∨ ((𝐴‘dom 𝐴) = 1o ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) = 2o) ∨ ((𝐴‘dom 𝐴) = ∅ ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) =
2o))) |
24 | | fvex 6782 |
. . . . 5
⊢ (𝐴‘dom 𝐴) ∈ V |
25 | | fvex 6782 |
. . . . 5
⊢ ((𝐴 ∪ {〈dom 𝐴,
2o〉})‘dom 𝐴) ∈ V |
26 | 24, 25 | brtp 33711 |
. . . 4
⊢ ((𝐴‘dom 𝐴){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ∪ {〈dom 𝐴,
2o〉})‘dom 𝐴) ↔ (((𝐴‘dom 𝐴) = 1o ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) = ∅) ∨ ((𝐴‘dom 𝐴) = 1o ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) = 2o) ∨ ((𝐴‘dom 𝐴) = ∅ ∧ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴) =
2o))) |
27 | 23, 26 | sylibr 233 |
. . 3
⊢ (𝐴 ∈
No → (𝐴‘dom 𝐴){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
((𝐴 ∪ {〈dom 𝐴,
2o〉})‘dom 𝐴)) |
28 | 10 | elexi 3450 |
. . . . . 6
⊢
2o ∈ V |
29 | 28 | prid2 4705 |
. . . . 5
⊢
2o ∈ {1o, 2o} |
30 | 29 | noextenddif 33865 |
. . . 4
⊢ (𝐴 ∈
No → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)} = dom 𝐴) |
31 | 30 | fveq2d 6773 |
. . 3
⊢ (𝐴 ∈
No → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}) = (𝐴‘dom 𝐴)) |
32 | 30 | fveq2d 6773 |
. . 3
⊢ (𝐴 ∈
No → ((𝐴 ∪
{〈dom 𝐴,
2o〉})‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}) = ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘dom 𝐴)) |
33 | 27, 31, 32 | 3brtr4d 5111 |
. 2
⊢ (𝐴 ∈
No → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}){〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉} ((𝐴
∪ {〈dom 𝐴,
2o〉})‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)})) |
34 | 29 | noextend 33863 |
. . 3
⊢ (𝐴 ∈
No → (𝐴 ∪
{〈dom 𝐴,
2o〉}) ∈ No
) |
35 | | sltval2 33853 |
. . 3
⊢ ((𝐴 ∈
No ∧ (𝐴 ∪
{〈dom 𝐴,
2o〉}) ∈ No ) → (𝐴 <s (𝐴 ∪ {〈dom 𝐴, 2o〉}) ↔ (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}){〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉} ((𝐴
∪ {〈dom 𝐴,
2o〉})‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}))) |
36 | 34, 35 | mpdan 684 |
. 2
⊢ (𝐴 ∈
No → (𝐴 <s
(𝐴 ∪ {〈dom 𝐴, 2o〉}) ↔
(𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}){〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉} ((𝐴
∪ {〈dom 𝐴,
2o〉})‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 2o〉})‘𝑥)}))) |
37 | 33, 36 | mpbird 256 |
1
⊢ (𝐴 ∈
No → 𝐴 <s
(𝐴 ∪ {〈dom 𝐴,
2o〉})) |