Step | Hyp | Ref
| Expression |
1 | | nofun 27149 |
. . 3
⊢ (𝐴 ∈
No → Fun 𝐴) |
2 | | dmexg 7893 |
. . . 4
⊢ (𝐴 ∈
No → dom 𝐴
∈ V) |
3 | | noextend.1 |
. . . 4
⊢ 𝑋 ∈ {1o,
2o} |
4 | | funsng 6599 |
. . . 4
⊢ ((dom
𝐴 ∈ V ∧ 𝑋 ∈ {1o,
2o}) → Fun {⟨dom 𝐴, 𝑋⟩}) |
5 | 2, 3, 4 | sylancl 586 |
. . 3
⊢ (𝐴 ∈
No → Fun {⟨dom 𝐴, 𝑋⟩}) |
6 | 3 | elexi 3493 |
. . . . . 6
⊢ 𝑋 ∈ V |
7 | 6 | dmsnop 6215 |
. . . . 5
⊢ dom
{⟨dom 𝐴, 𝑋⟩} = {dom 𝐴} |
8 | 7 | ineq2i 4209 |
. . . 4
⊢ (dom
𝐴 ∩ dom {⟨dom
𝐴, 𝑋⟩}) = (dom 𝐴 ∩ {dom 𝐴}) |
9 | | nodmord 27153 |
. . . . . 6
⊢ (𝐴 ∈
No → Ord dom 𝐴) |
10 | | ordirr 6382 |
. . . . . 6
⊢ (Ord dom
𝐴 → ¬ dom 𝐴 ∈ dom 𝐴) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ (𝐴 ∈
No → ¬ dom 𝐴 ∈ dom 𝐴) |
12 | | disjsn 4715 |
. . . . 5
⊢ ((dom
𝐴 ∩ {dom 𝐴}) = ∅ ↔ ¬ dom
𝐴 ∈ dom 𝐴) |
13 | 11, 12 | sylibr 233 |
. . . 4
⊢ (𝐴 ∈
No → (dom 𝐴
∩ {dom 𝐴}) =
∅) |
14 | 8, 13 | eqtrid 2784 |
. . 3
⊢ (𝐴 ∈
No → (dom 𝐴
∩ dom {⟨dom 𝐴,
𝑋⟩}) =
∅) |
15 | | funun 6594 |
. . 3
⊢ (((Fun
𝐴 ∧ Fun {⟨dom
𝐴, 𝑋⟩}) ∧ (dom 𝐴 ∩ dom {⟨dom 𝐴, 𝑋⟩}) = ∅) → Fun (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩})) |
16 | 1, 5, 14, 15 | syl21anc 836 |
. 2
⊢ (𝐴 ∈
No → Fun (𝐴
∪ {⟨dom 𝐴, 𝑋⟩})) |
17 | 7 | uneq2i 4160 |
. . . 4
⊢ (dom
𝐴 ∪ dom {⟨dom
𝐴, 𝑋⟩}) = (dom 𝐴 ∪ {dom 𝐴}) |
18 | | dmun 5910 |
. . . 4
⊢ dom
(𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) = (dom 𝐴 ∪ dom {⟨dom 𝐴, 𝑋⟩}) |
19 | | df-suc 6370 |
. . . 4
⊢ suc dom
𝐴 = (dom 𝐴 ∪ {dom 𝐴}) |
20 | 17, 18, 19 | 3eqtr4i 2770 |
. . 3
⊢ dom
(𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) = suc dom 𝐴 |
21 | | nodmon 27150 |
. . . 4
⊢ (𝐴 ∈
No → dom 𝐴
∈ On) |
22 | | onsuc 7798 |
. . . 4
⊢ (dom
𝐴 ∈ On → suc dom
𝐴 ∈
On) |
23 | 21, 22 | syl 17 |
. . 3
⊢ (𝐴 ∈
No → suc dom 𝐴
∈ On) |
24 | 20, 23 | eqeltrid 2837 |
. 2
⊢ (𝐴 ∈
No → dom (𝐴
∪ {⟨dom 𝐴, 𝑋⟩}) ∈
On) |
25 | | rnun 6145 |
. . . 4
⊢ ran
(𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) = (ran 𝐴 ∪ ran {⟨dom 𝐴, 𝑋⟩}) |
26 | | rnsnopg 6220 |
. . . . . 6
⊢ (dom
𝐴 ∈ V → ran
{⟨dom 𝐴, 𝑋⟩} = {𝑋}) |
27 | 2, 26 | syl 17 |
. . . . 5
⊢ (𝐴 ∈
No → ran {⟨dom 𝐴, 𝑋⟩} = {𝑋}) |
28 | 27 | uneq2d 4163 |
. . . 4
⊢ (𝐴 ∈
No → (ran 𝐴
∪ ran {⟨dom 𝐴,
𝑋⟩}) = (ran 𝐴 ∪ {𝑋})) |
29 | 25, 28 | eqtrid 2784 |
. . 3
⊢ (𝐴 ∈
No → ran (𝐴
∪ {⟨dom 𝐴, 𝑋⟩}) = (ran 𝐴 ∪ {𝑋})) |
30 | | norn 27151 |
. . . 4
⊢ (𝐴 ∈
No → ran 𝐴
⊆ {1o, 2o}) |
31 | | snssi 4811 |
. . . . 5
⊢ (𝑋 ∈ {1o,
2o} → {𝑋}
⊆ {1o, 2o}) |
32 | 3, 31 | mp1i 13 |
. . . 4
⊢ (𝐴 ∈
No → {𝑋}
⊆ {1o, 2o}) |
33 | 30, 32 | unssd 4186 |
. . 3
⊢ (𝐴 ∈
No → (ran 𝐴
∪ {𝑋}) ⊆
{1o, 2o}) |
34 | 29, 33 | eqsstrd 4020 |
. 2
⊢ (𝐴 ∈
No → ran (𝐴
∪ {⟨dom 𝐴, 𝑋⟩}) ⊆ {1o,
2o}) |
35 | | elno2 27154 |
. 2
⊢ ((𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ No
↔ (Fun (𝐴
∪ {⟨dom 𝐴, 𝑋⟩}) ∧ dom (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ On ∧ ran (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ⊆ {1o,
2o})) |
36 | 16, 24, 34, 35 | syl3anbrc 1343 |
1
⊢ (𝐴 ∈
No → (𝐴 ∪
{⟨dom 𝐴, 𝑋⟩}) ∈ No ) |