Step | Hyp | Ref
| Expression |
1 | | nofun 27020 |
. . 3
⊢ (𝐴 ∈
No → Fun 𝐴) |
2 | | dmexg 7844 |
. . . 4
⊢ (𝐴 ∈
No → dom 𝐴
∈ V) |
3 | | noextend.1 |
. . . 4
⊢ 𝑋 ∈ {1o,
2o} |
4 | | funsng 6556 |
. . . 4
⊢ ((dom
𝐴 ∈ V ∧ 𝑋 ∈ {1o,
2o}) → Fun {⟨dom 𝐴, 𝑋⟩}) |
5 | 2, 3, 4 | sylancl 587 |
. . 3
⊢ (𝐴 ∈
No → Fun {⟨dom 𝐴, 𝑋⟩}) |
6 | 3 | elexi 3466 |
. . . . . 6
⊢ 𝑋 ∈ V |
7 | 6 | dmsnop 6172 |
. . . . 5
⊢ dom
{⟨dom 𝐴, 𝑋⟩} = {dom 𝐴} |
8 | 7 | ineq2i 4173 |
. . . 4
⊢ (dom
𝐴 ∩ dom {⟨dom
𝐴, 𝑋⟩}) = (dom 𝐴 ∩ {dom 𝐴}) |
9 | | nodmord 27024 |
. . . . . 6
⊢ (𝐴 ∈
No → Ord dom 𝐴) |
10 | | ordirr 6339 |
. . . . . 6
⊢ (Ord dom
𝐴 → ¬ dom 𝐴 ∈ dom 𝐴) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ (𝐴 ∈
No → ¬ dom 𝐴 ∈ dom 𝐴) |
12 | | disjsn 4676 |
. . . . 5
⊢ ((dom
𝐴 ∩ {dom 𝐴}) = ∅ ↔ ¬ dom
𝐴 ∈ dom 𝐴) |
13 | 11, 12 | sylibr 233 |
. . . 4
⊢ (𝐴 ∈
No → (dom 𝐴
∩ {dom 𝐴}) =
∅) |
14 | 8, 13 | eqtrid 2785 |
. . 3
⊢ (𝐴 ∈
No → (dom 𝐴
∩ dom {⟨dom 𝐴,
𝑋⟩}) =
∅) |
15 | | funun 6551 |
. . 3
⊢ (((Fun
𝐴 ∧ Fun {⟨dom
𝐴, 𝑋⟩}) ∧ (dom 𝐴 ∩ dom {⟨dom 𝐴, 𝑋⟩}) = ∅) → Fun (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩})) |
16 | 1, 5, 14, 15 | syl21anc 837 |
. 2
⊢ (𝐴 ∈
No → Fun (𝐴
∪ {⟨dom 𝐴, 𝑋⟩})) |
17 | 7 | uneq2i 4124 |
. . . 4
⊢ (dom
𝐴 ∪ dom {⟨dom
𝐴, 𝑋⟩}) = (dom 𝐴 ∪ {dom 𝐴}) |
18 | | dmun 5870 |
. . . 4
⊢ dom
(𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) = (dom 𝐴 ∪ dom {⟨dom 𝐴, 𝑋⟩}) |
19 | | df-suc 6327 |
. . . 4
⊢ suc dom
𝐴 = (dom 𝐴 ∪ {dom 𝐴}) |
20 | 17, 18, 19 | 3eqtr4i 2771 |
. . 3
⊢ dom
(𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) = suc dom 𝐴 |
21 | | nodmon 27021 |
. . . 4
⊢ (𝐴 ∈
No → dom 𝐴
∈ On) |
22 | | onsuc 7750 |
. . . 4
⊢ (dom
𝐴 ∈ On → suc dom
𝐴 ∈
On) |
23 | 21, 22 | syl 17 |
. . 3
⊢ (𝐴 ∈
No → suc dom 𝐴
∈ On) |
24 | 20, 23 | eqeltrid 2838 |
. 2
⊢ (𝐴 ∈
No → dom (𝐴
∪ {⟨dom 𝐴, 𝑋⟩}) ∈
On) |
25 | | rnun 6102 |
. . . 4
⊢ ran
(𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) = (ran 𝐴 ∪ ran {⟨dom 𝐴, 𝑋⟩}) |
26 | | rnsnopg 6177 |
. . . . . 6
⊢ (dom
𝐴 ∈ V → ran
{⟨dom 𝐴, 𝑋⟩} = {𝑋}) |
27 | 2, 26 | syl 17 |
. . . . 5
⊢ (𝐴 ∈
No → ran {⟨dom 𝐴, 𝑋⟩} = {𝑋}) |
28 | 27 | uneq2d 4127 |
. . . 4
⊢ (𝐴 ∈
No → (ran 𝐴
∪ ran {⟨dom 𝐴,
𝑋⟩}) = (ran 𝐴 ∪ {𝑋})) |
29 | 25, 28 | eqtrid 2785 |
. . 3
⊢ (𝐴 ∈
No → ran (𝐴
∪ {⟨dom 𝐴, 𝑋⟩}) = (ran 𝐴 ∪ {𝑋})) |
30 | | norn 27022 |
. . . 4
⊢ (𝐴 ∈
No → ran 𝐴
⊆ {1o, 2o}) |
31 | | snssi 4772 |
. . . . 5
⊢ (𝑋 ∈ {1o,
2o} → {𝑋}
⊆ {1o, 2o}) |
32 | 3, 31 | mp1i 13 |
. . . 4
⊢ (𝐴 ∈
No → {𝑋}
⊆ {1o, 2o}) |
33 | 30, 32 | unssd 4150 |
. . 3
⊢ (𝐴 ∈
No → (ran 𝐴
∪ {𝑋}) ⊆
{1o, 2o}) |
34 | 29, 33 | eqsstrd 3986 |
. 2
⊢ (𝐴 ∈
No → ran (𝐴
∪ {⟨dom 𝐴, 𝑋⟩}) ⊆ {1o,
2o}) |
35 | | elno2 27025 |
. 2
⊢ ((𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ No
↔ (Fun (𝐴
∪ {⟨dom 𝐴, 𝑋⟩}) ∧ dom (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ On ∧ ran (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ⊆ {1o,
2o})) |
36 | 16, 24, 34, 35 | syl3anbrc 1344 |
1
⊢ (𝐴 ∈
No → (𝐴 ∪
{⟨dom 𝐴, 𝑋⟩}) ∈ No ) |