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