Step |
Hyp |
Ref |
Expression |
1 |
|
nodmord |
⊢ ( 𝐴 ∈ No → Ord dom 𝐴 ) |
2 |
|
ordirr |
⊢ ( Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴 ) |
3 |
1 2
|
syl |
⊢ ( 𝐴 ∈ No → ¬ dom 𝐴 ∈ dom 𝐴 ) |
4 |
|
ndmfv |
⊢ ( ¬ dom 𝐴 ∈ dom 𝐴 → ( 𝐴 ‘ dom 𝐴 ) = ∅ ) |
5 |
3 4
|
syl |
⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ dom 𝐴 ) = ∅ ) |
6 |
|
nofun |
⊢ ( 𝐴 ∈ No → Fun 𝐴 ) |
7 |
|
funfn |
⊢ ( Fun 𝐴 ↔ 𝐴 Fn dom 𝐴 ) |
8 |
6 7
|
sylib |
⊢ ( 𝐴 ∈ No → 𝐴 Fn dom 𝐴 ) |
9 |
|
nodmon |
⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On ) |
10 |
|
2on |
⊢ 2o ∈ On |
11 |
|
fnsng |
⊢ ( ( dom 𝐴 ∈ On ∧ 2o ∈ On ) → { 〈 dom 𝐴 , 2o 〉 } Fn { dom 𝐴 } ) |
12 |
9 10 11
|
sylancl |
⊢ ( 𝐴 ∈ No → { 〈 dom 𝐴 , 2o 〉 } Fn { dom 𝐴 } ) |
13 |
|
disjsn |
⊢ ( ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ↔ ¬ dom 𝐴 ∈ dom 𝐴 ) |
14 |
3 13
|
sylibr |
⊢ ( 𝐴 ∈ No → ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ) |
15 |
|
snidg |
⊢ ( dom 𝐴 ∈ On → dom 𝐴 ∈ { dom 𝐴 } ) |
16 |
9 15
|
syl |
⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ { dom 𝐴 } ) |
17 |
|
fvun2 |
⊢ ( ( 𝐴 Fn dom 𝐴 ∧ { 〈 dom 𝐴 , 2o 〉 } Fn { dom 𝐴 } ∧ ( ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ∧ dom 𝐴 ∈ { dom 𝐴 } ) ) → ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ dom 𝐴 ) = ( { 〈 dom 𝐴 , 2o 〉 } ‘ dom 𝐴 ) ) |
18 |
8 12 14 16 17
|
syl112anc |
⊢ ( 𝐴 ∈ No → ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ dom 𝐴 ) = ( { 〈 dom 𝐴 , 2o 〉 } ‘ dom 𝐴 ) ) |
19 |
|
fvsng |
⊢ ( ( dom 𝐴 ∈ On ∧ 2o ∈ On ) → ( { 〈 dom 𝐴 , 2o 〉 } ‘ dom 𝐴 ) = 2o ) |
20 |
9 10 19
|
sylancl |
⊢ ( 𝐴 ∈ No → ( { 〈 dom 𝐴 , 2o 〉 } ‘ dom 𝐴 ) = 2o ) |
21 |
18 20
|
eqtrd |
⊢ ( 𝐴 ∈ No → ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ dom 𝐴 ) = 2o ) |
22 |
5 21
|
jca |
⊢ ( 𝐴 ∈ No → ( ( 𝐴 ‘ dom 𝐴 ) = ∅ ∧ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ dom 𝐴 ) = 2o ) ) |
23 |
22
|
3mix3d |
⊢ ( 𝐴 ∈ No → ( ( ( 𝐴 ‘ dom 𝐴 ) = 1o ∧ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ dom 𝐴 ) = ∅ ) ∨ ( ( 𝐴 ‘ dom 𝐴 ) = 1o ∧ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ dom 𝐴 ) = 2o ) ∨ ( ( 𝐴 ‘ dom 𝐴 ) = ∅ ∧ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ dom 𝐴 ) = 2o ) ) ) |
24 |
|
fvex |
⊢ ( 𝐴 ‘ dom 𝐴 ) ∈ V |
25 |
|
fvex |
⊢ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ dom 𝐴 ) ∈ V |
26 |
24 25
|
brtp |
⊢ ( ( 𝐴 ‘ 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 |
⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ dom 𝐴 ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ dom 𝐴 ) ) |
28 |
10
|
elexi |
⊢ 2o ∈ V |
29 |
28
|
prid2 |
⊢ 2o ∈ { 1o , 2o } |
30 |
29
|
noextenddif |
⊢ ( 𝐴 ∈ No → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ 𝑥 ) } = dom 𝐴 ) |
31 |
30
|
fveq2d |
⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ 𝑥 ) } ) = ( 𝐴 ‘ dom 𝐴 ) ) |
32 |
30
|
fveq2d |
⊢ ( 𝐴 ∈ No → ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ 𝑥 ) } ) = ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ dom 𝐴 ) ) |
33 |
27 31 32
|
3brtr4d |
⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ 𝑥 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ 𝑥 ) } ) ) |
34 |
29
|
noextend |
⊢ ( 𝐴 ∈ No → ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ∈ No ) |
35 |
|
sltval2 |
⊢ ( ( 𝐴 ∈ No ∧ ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ∈ No ) → ( 𝐴 <s ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ↔ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ 𝑥 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ 𝑥 ) } ) ) ) |
36 |
34 35
|
mpdan |
⊢ ( 𝐴 ∈ No → ( 𝐴 <s ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ↔ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ 𝑥 ) } ) { 〈 1o , ∅ 〉 , 〈 1o , 2o 〉 , 〈 ∅ , 2o 〉 } ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ‘ 𝑥 ) } ) ) ) |
37 |
33 36
|
mpbird |
⊢ ( 𝐴 ∈ No → 𝐴 <s ( 𝐴 ∪ { 〈 dom 𝐴 , 2o 〉 } ) ) |