Step |
Hyp |
Ref |
Expression |
1 |
|
noextend.1 |
⊢ 𝑋 ∈ { 1o , 2o } |
2 |
|
nofun |
⊢ ( 𝐴 ∈ No → Fun 𝐴 ) |
3 |
|
dmexg |
⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ V ) |
4 |
|
funsng |
⊢ ( ( dom 𝐴 ∈ V ∧ 𝑋 ∈ { 1o , 2o } ) → Fun { 〈 dom 𝐴 , 𝑋 〉 } ) |
5 |
3 1 4
|
sylancl |
⊢ ( 𝐴 ∈ No → Fun { 〈 dom 𝐴 , 𝑋 〉 } ) |
6 |
1
|
elexi |
⊢ 𝑋 ∈ V |
7 |
6
|
dmsnop |
⊢ dom { 〈 dom 𝐴 , 𝑋 〉 } = { dom 𝐴 } |
8 |
7
|
ineq2i |
⊢ ( dom 𝐴 ∩ dom { 〈 dom 𝐴 , 𝑋 〉 } ) = ( dom 𝐴 ∩ { dom 𝐴 } ) |
9 |
|
nodmord |
⊢ ( 𝐴 ∈ No → Ord dom 𝐴 ) |
10 |
|
ordirr |
⊢ ( Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴 ) |
11 |
9 10
|
syl |
⊢ ( 𝐴 ∈ No → ¬ dom 𝐴 ∈ dom 𝐴 ) |
12 |
|
disjsn |
⊢ ( ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ↔ ¬ dom 𝐴 ∈ dom 𝐴 ) |
13 |
11 12
|
sylibr |
⊢ ( 𝐴 ∈ No → ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ) |
14 |
8 13
|
syl5eq |
⊢ ( 𝐴 ∈ No → ( dom 𝐴 ∩ dom { 〈 dom 𝐴 , 𝑋 〉 } ) = ∅ ) |
15 |
|
funun |
⊢ ( ( ( Fun 𝐴 ∧ Fun { 〈 dom 𝐴 , 𝑋 〉 } ) ∧ ( dom 𝐴 ∩ dom { 〈 dom 𝐴 , 𝑋 〉 } ) = ∅ ) → Fun ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) ) |
16 |
2 5 14 15
|
syl21anc |
⊢ ( 𝐴 ∈ No → Fun ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) ) |
17 |
7
|
uneq2i |
⊢ ( dom 𝐴 ∪ dom { 〈 dom 𝐴 , 𝑋 〉 } ) = ( dom 𝐴 ∪ { dom 𝐴 } ) |
18 |
|
dmun |
⊢ dom ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) = ( dom 𝐴 ∪ dom { 〈 dom 𝐴 , 𝑋 〉 } ) |
19 |
|
df-suc |
⊢ suc dom 𝐴 = ( dom 𝐴 ∪ { dom 𝐴 } ) |
20 |
17 18 19
|
3eqtr4i |
⊢ dom ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) = suc dom 𝐴 |
21 |
|
nodmon |
⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On ) |
22 |
|
suceloni |
⊢ ( dom 𝐴 ∈ On → suc dom 𝐴 ∈ On ) |
23 |
21 22
|
syl |
⊢ ( 𝐴 ∈ No → suc dom 𝐴 ∈ On ) |
24 |
20 23
|
eqeltrid |
⊢ ( 𝐴 ∈ No → dom ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) ∈ On ) |
25 |
|
rnun |
⊢ ran ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) = ( ran 𝐴 ∪ ran { 〈 dom 𝐴 , 𝑋 〉 } ) |
26 |
|
rnsnopg |
⊢ ( dom 𝐴 ∈ V → ran { 〈 dom 𝐴 , 𝑋 〉 } = { 𝑋 } ) |
27 |
3 26
|
syl |
⊢ ( 𝐴 ∈ No → ran { 〈 dom 𝐴 , 𝑋 〉 } = { 𝑋 } ) |
28 |
27
|
uneq2d |
⊢ ( 𝐴 ∈ No → ( ran 𝐴 ∪ ran { 〈 dom 𝐴 , 𝑋 〉 } ) = ( ran 𝐴 ∪ { 𝑋 } ) ) |
29 |
25 28
|
syl5eq |
⊢ ( 𝐴 ∈ No → ran ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) = ( ran 𝐴 ∪ { 𝑋 } ) ) |
30 |
|
norn |
⊢ ( 𝐴 ∈ No → ran 𝐴 ⊆ { 1o , 2o } ) |
31 |
|
snssi |
⊢ ( 𝑋 ∈ { 1o , 2o } → { 𝑋 } ⊆ { 1o , 2o } ) |
32 |
1 31
|
mp1i |
⊢ ( 𝐴 ∈ No → { 𝑋 } ⊆ { 1o , 2o } ) |
33 |
30 32
|
unssd |
⊢ ( 𝐴 ∈ No → ( ran 𝐴 ∪ { 𝑋 } ) ⊆ { 1o , 2o } ) |
34 |
29 33
|
eqsstrd |
⊢ ( 𝐴 ∈ No → ran ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) ⊆ { 1o , 2o } ) |
35 |
|
elno2 |
⊢ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) ∈ No ↔ ( Fun ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) ∧ dom ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) ∈ On ∧ ran ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) ⊆ { 1o , 2o } ) ) |
36 |
16 24 34 35
|
syl3anbrc |
⊢ ( 𝐴 ∈ No → ( 𝐴 ∪ { 〈 dom 𝐴 , 𝑋 〉 } ) ∈ No ) |