Step | Hyp | Ref
| Expression |
1 | | nofun 33493 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → Fun 𝐴) |
2 | | funfn 6369 |
. . . . . . . . 9
⊢ (Fun
𝐴 ↔ 𝐴 Fn dom 𝐴) |
3 | 1, 2 | sylib 221 |
. . . . . . . 8
⊢ (𝐴 ∈
No → 𝐴 Fn dom
𝐴) |
4 | | nodmon 33494 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → dom 𝐴
∈ On) |
5 | | 1on 8138 |
. . . . . . . . 9
⊢
1o ∈ On |
6 | | fnsng 6391 |
. . . . . . . . 9
⊢ ((dom
𝐴 ∈ On ∧
1o ∈ On) → {〈dom 𝐴, 1o〉} Fn {dom 𝐴}) |
7 | 4, 5, 6 | sylancl 589 |
. . . . . . . 8
⊢ (𝐴 ∈
No → {〈dom 𝐴, 1o〉} Fn {dom 𝐴}) |
8 | | nodmord 33497 |
. . . . . . . . . 10
⊢ (𝐴 ∈
No → Ord dom 𝐴) |
9 | | ordirr 6190 |
. . . . . . . . . 10
⊢ (Ord dom
𝐴 → ¬ dom 𝐴 ∈ dom 𝐴) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → ¬ dom 𝐴 ∈ dom 𝐴) |
11 | | disjsn 4602 |
. . . . . . . . 9
⊢ ((dom
𝐴 ∩ {dom 𝐴}) = ∅ ↔ ¬ dom
𝐴 ∈ dom 𝐴) |
12 | 10, 11 | sylibr 237 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (dom 𝐴
∩ {dom 𝐴}) =
∅) |
13 | | snidg 4550 |
. . . . . . . . 9
⊢ (dom
𝐴 ∈ On → dom
𝐴 ∈ {dom 𝐴}) |
14 | 4, 13 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈
No → dom 𝐴
∈ {dom 𝐴}) |
15 | | fvun2 6760 |
. . . . . . . 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 6952 |
. . . . . . . 8
⊢ ((dom
𝐴 ∈ On ∧
1o ∈ On) → ({〈dom 𝐴, 1o〉}‘dom 𝐴) =
1o) |
18 | 4, 5, 17 | sylancl 589 |
. . . . . . 7
⊢ (𝐴 ∈
No → ({〈dom 𝐴, 1o〉}‘dom 𝐴) =
1o) |
19 | 16, 18 | eqtrd 2773 |
. . . . . 6
⊢ (𝐴 ∈
No → ((𝐴 ∪
{〈dom 𝐴,
1o〉})‘dom 𝐴) = 1o) |
20 | | ndmfv 6704 |
. . . . . . 7
⊢ (¬
dom 𝐴 ∈ dom 𝐴 → (𝐴‘dom 𝐴) = ∅) |
21 | 10, 20 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈
No → (𝐴‘dom 𝐴) = ∅) |
22 | 19, 21 | jca 515 |
. . . . 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 6687 |
. . . . 5
⊢ ((𝐴 ∪ {〈dom 𝐴,
1o〉})‘dom 𝐴) ∈ V |
25 | | fvex 6687 |
. . . . 5
⊢ (𝐴‘dom 𝐴) ∈ V |
26 | 24, 25 | brtp 33288 |
. . . 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 237 |
. . 3
⊢ (𝐴 ∈
No → ((𝐴 ∪
{〈dom 𝐴,
1o〉})‘dom 𝐴){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐴‘dom 𝐴)) |
28 | | necom 2987 |
. . . . . . 7
⊢ (((𝐴 ∪ {〈dom 𝐴,
1o〉})‘𝑥) ≠ (𝐴‘𝑥) ↔ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 1o〉})‘𝑥)) |
29 | 28 | rabbii 3374 |
. . . . . 6
⊢ {𝑥 ∈ On ∣ ((𝐴 ∪ {〈dom 𝐴,
1o〉})‘𝑥) ≠ (𝐴‘𝑥)} = {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 1o〉})‘𝑥)} |
30 | 29 | inteqi 4840 |
. . . . 5
⊢ ∩ {𝑥
∈ On ∣ ((𝐴 ∪
{〈dom 𝐴,
1o〉})‘𝑥) ≠ (𝐴‘𝑥)} = ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 1o〉})‘𝑥)} |
31 | | 1oex 8144 |
. . . . . . 7
⊢
1o ∈ V |
32 | 31 | prid1 4653 |
. . . . . 6
⊢
1o ∈ {1o, 2o} |
33 | 32 | noextenddif 33512 |
. . . . 5
⊢ (𝐴 ∈
No → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {〈dom 𝐴, 1o〉})‘𝑥)} = dom 𝐴) |
34 | 30, 33 | syl5eq 2785 |
. . . 4
⊢ (𝐴 ∈
No → ∩ {𝑥 ∈ On ∣ ((𝐴 ∪ {〈dom 𝐴, 1o〉})‘𝑥) ≠ (𝐴‘𝑥)} = dom 𝐴) |
35 | 34 | fveq2d 6678 |
. . 3
⊢ (𝐴 ∈
No → ((𝐴 ∪
{〈dom 𝐴,
1o〉})‘∩ {𝑥 ∈ On ∣ ((𝐴 ∪ {〈dom 𝐴, 1o〉})‘𝑥) ≠ (𝐴‘𝑥)}) = ((𝐴 ∪ {〈dom 𝐴, 1o〉})‘dom 𝐴)) |
36 | 34 | fveq2d 6678 |
. . 3
⊢ (𝐴 ∈
No → (𝐴‘∩ {𝑥 ∈ On ∣ ((𝐴 ∪ {〈dom 𝐴,
1o〉})‘𝑥) ≠ (𝐴‘𝑥)}) = (𝐴‘dom 𝐴)) |
37 | 27, 35, 36 | 3brtr4d 5062 |
. 2
⊢ (𝐴 ∈
No → ((𝐴 ∪
{〈dom 𝐴,
1o〉})‘∩ {𝑥 ∈ On ∣ ((𝐴 ∪ {〈dom 𝐴, 1o〉})‘𝑥) ≠ (𝐴‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐴‘∩ {𝑥
∈ On ∣ ((𝐴 ∪
{〈dom 𝐴,
1o〉})‘𝑥) ≠ (𝐴‘𝑥)})) |
38 | 32 | noextend 33510 |
. . 3
⊢ (𝐴 ∈
No → (𝐴 ∪
{〈dom 𝐴,
1o〉}) ∈ No
) |
39 | | sltval2 33500 |
. . 3
⊢ (((𝐴 ∪ {〈dom 𝐴, 1o〉}) ∈
No ∧ 𝐴 ∈ No )
→ ((𝐴 ∪ {〈dom
𝐴, 1o〉})
<s 𝐴 ↔ ((𝐴 ∪ {〈dom 𝐴,
1o〉})‘∩ {𝑥 ∈ On ∣ ((𝐴 ∪ {〈dom 𝐴, 1o〉})‘𝑥) ≠ (𝐴‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐴‘∩ {𝑥
∈ On ∣ ((𝐴 ∪
{〈dom 𝐴,
1o〉})‘𝑥) ≠ (𝐴‘𝑥)}))) |
40 | 38, 39 | mpancom 688 |
. 2
⊢ (𝐴 ∈
No → ((𝐴 ∪
{〈dom 𝐴,
1o〉}) <s 𝐴 ↔ ((𝐴 ∪ {〈dom 𝐴, 1o〉})‘∩ {𝑥
∈ On ∣ ((𝐴 ∪
{〈dom 𝐴,
1o〉})‘𝑥) ≠ (𝐴‘𝑥)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐴‘∩ {𝑥
∈ On ∣ ((𝐴 ∪
{〈dom 𝐴,
1o〉})‘𝑥) ≠ (𝐴‘𝑥)}))) |
41 | 37, 40 | mpbird 260 |
1
⊢ (𝐴 ∈
No → (𝐴 ∪
{〈dom 𝐴,
1o〉}) <s 𝐴) |