| Step |
Hyp |
Ref |
Expression |
| 1 |
|
harval2 |
⊢ ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) = ∩ { 𝑦 ∈ On ∣ 𝐴 ≺ 𝑦 } ) |
| 2 |
|
vex |
⊢ 𝑥 ∈ V |
| 3 |
2
|
a1i |
⊢ ( 𝐴 ∈ dom card → 𝑥 ∈ V ) |
| 4 |
|
elrncard |
⊢ ( 𝑥 ∈ ran card ↔ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ¬ 𝑦 ≈ 𝑥 ) ) |
| 5 |
4
|
simplbi |
⊢ ( 𝑥 ∈ ran card → 𝑥 ∈ On ) |
| 6 |
5
|
anim1i |
⊢ ( ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) → ( 𝑥 ∈ On ∧ 𝐴 ≺ 𝑥 ) ) |
| 7 |
|
eleq1 |
⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ On ↔ 𝑥 ∈ On ) ) |
| 8 |
|
breq2 |
⊢ ( 𝑦 = 𝑥 → ( 𝐴 ≺ 𝑦 ↔ 𝐴 ≺ 𝑥 ) ) |
| 9 |
7 8
|
anbi12d |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) ↔ ( 𝑥 ∈ On ∧ 𝐴 ≺ 𝑥 ) ) ) |
| 10 |
6 9
|
imbitrrid |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) → ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) ) ) |
| 11 |
10
|
adantl |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝑦 = 𝑥 ) → ( ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) → ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) ) ) |
| 12 |
|
ssidd |
⊢ ( 𝐴 ∈ dom card → 𝑥 ⊆ 𝑥 ) |
| 13 |
3 11 12
|
intabssd |
⊢ ( 𝐴 ∈ dom card → ∩ { 𝑦 ∣ ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) } ⊆ ∩ { 𝑥 ∣ ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) } ) |
| 14 |
|
vex |
⊢ 𝑦 ∈ V |
| 15 |
14
|
inex1 |
⊢ ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ∈ V |
| 16 |
15
|
a1i |
⊢ ( 𝐴 ∈ dom card → ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ∈ V ) |
| 17 |
|
oncardid |
⊢ ( 𝑦 ∈ On → ( card ‘ 𝑦 ) ≈ 𝑦 ) |
| 18 |
17
|
ensymd |
⊢ ( 𝑦 ∈ On → 𝑦 ≈ ( card ‘ 𝑦 ) ) |
| 19 |
|
sdomentr |
⊢ ( ( 𝐴 ≺ 𝑦 ∧ 𝑦 ≈ ( card ‘ 𝑦 ) ) → 𝐴 ≺ ( card ‘ 𝑦 ) ) |
| 20 |
19
|
a1i |
⊢ ( 𝑦 ∈ On → ( ( 𝐴 ≺ 𝑦 ∧ 𝑦 ≈ ( card ‘ 𝑦 ) ) → 𝐴 ≺ ( card ‘ 𝑦 ) ) ) |
| 21 |
18 20
|
mpan2d |
⊢ ( 𝑦 ∈ On → ( 𝐴 ≺ 𝑦 → 𝐴 ≺ ( card ‘ 𝑦 ) ) ) |
| 22 |
|
df-card |
⊢ card = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ On ∣ 𝑦 ≈ 𝑥 } ) |
| 23 |
22
|
funmpt2 |
⊢ Fun card |
| 24 |
|
onenon |
⊢ ( 𝑦 ∈ On → 𝑦 ∈ dom card ) |
| 25 |
|
fvelrn |
⊢ ( ( Fun card ∧ 𝑦 ∈ dom card ) → ( card ‘ 𝑦 ) ∈ ran card ) |
| 26 |
23 24 25
|
sylancr |
⊢ ( 𝑦 ∈ On → ( card ‘ 𝑦 ) ∈ ran card ) |
| 27 |
21 26
|
jctild |
⊢ ( 𝑦 ∈ On → ( 𝐴 ≺ 𝑦 → ( ( card ‘ 𝑦 ) ∈ ran card ∧ 𝐴 ≺ ( card ‘ 𝑦 ) ) ) ) |
| 28 |
27
|
adantl |
⊢ ( ( 𝑥 = ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ∧ 𝑦 ∈ On ) → ( 𝐴 ≺ 𝑦 → ( ( card ‘ 𝑦 ) ∈ ran card ∧ 𝐴 ≺ ( card ‘ 𝑦 ) ) ) ) |
| 29 |
|
simpl |
⊢ ( ( 𝑥 = ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ∧ 𝑦 ∈ On ) → 𝑥 = ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ) |
| 30 |
|
cardonle |
⊢ ( 𝑦 ∈ On → ( card ‘ 𝑦 ) ⊆ 𝑦 ) |
| 31 |
30
|
adantl |
⊢ ( ( 𝑥 = ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ∧ 𝑦 ∈ On ) → ( card ‘ 𝑦 ) ⊆ 𝑦 ) |
| 32 |
|
sseqin2 |
⊢ ( ( card ‘ 𝑦 ) ⊆ 𝑦 ↔ ( 𝑦 ∩ ( card ‘ 𝑦 ) ) = ( card ‘ 𝑦 ) ) |
| 33 |
31 32
|
sylib |
⊢ ( ( 𝑥 = ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ∧ 𝑦 ∈ On ) → ( 𝑦 ∩ ( card ‘ 𝑦 ) ) = ( card ‘ 𝑦 ) ) |
| 34 |
29 33
|
eqtrd |
⊢ ( ( 𝑥 = ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ∧ 𝑦 ∈ On ) → 𝑥 = ( card ‘ 𝑦 ) ) |
| 35 |
|
eleq1 |
⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( 𝑥 ∈ ran card ↔ ( card ‘ 𝑦 ) ∈ ran card ) ) |
| 36 |
|
breq2 |
⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( 𝐴 ≺ 𝑥 ↔ 𝐴 ≺ ( card ‘ 𝑦 ) ) ) |
| 37 |
35 36
|
anbi12d |
⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) ↔ ( ( card ‘ 𝑦 ) ∈ ran card ∧ 𝐴 ≺ ( card ‘ 𝑦 ) ) ) ) |
| 38 |
34 37
|
syl |
⊢ ( ( 𝑥 = ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ∧ 𝑦 ∈ On ) → ( ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) ↔ ( ( card ‘ 𝑦 ) ∈ ran card ∧ 𝐴 ≺ ( card ‘ 𝑦 ) ) ) ) |
| 39 |
28 38
|
sylibrd |
⊢ ( ( 𝑥 = ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ∧ 𝑦 ∈ On ) → ( 𝐴 ≺ 𝑦 → ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) ) ) |
| 40 |
39
|
expimpd |
⊢ ( 𝑥 = ( 𝑦 ∩ ( card ‘ 𝑦 ) ) → ( ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) → ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) ) ) |
| 41 |
40
|
adantl |
⊢ ( ( 𝐴 ∈ dom card ∧ 𝑥 = ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ) → ( ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) → ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) ) ) |
| 42 |
|
inss1 |
⊢ ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ⊆ 𝑦 |
| 43 |
42
|
a1i |
⊢ ( 𝐴 ∈ dom card → ( 𝑦 ∩ ( card ‘ 𝑦 ) ) ⊆ 𝑦 ) |
| 44 |
16 41 43
|
intabssd |
⊢ ( 𝐴 ∈ dom card → ∩ { 𝑥 ∣ ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) } ⊆ ∩ { 𝑦 ∣ ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) } ) |
| 45 |
13 44
|
eqssd |
⊢ ( 𝐴 ∈ dom card → ∩ { 𝑦 ∣ ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) } = ∩ { 𝑥 ∣ ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) } ) |
| 46 |
|
df-rab |
⊢ { 𝑦 ∈ On ∣ 𝐴 ≺ 𝑦 } = { 𝑦 ∣ ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) } |
| 47 |
46
|
inteqi |
⊢ ∩ { 𝑦 ∈ On ∣ 𝐴 ≺ 𝑦 } = ∩ { 𝑦 ∣ ( 𝑦 ∈ On ∧ 𝐴 ≺ 𝑦 ) } |
| 48 |
|
df-rab |
⊢ { 𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) } |
| 49 |
48
|
inteqi |
⊢ ∩ { 𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥 } = ∩ { 𝑥 ∣ ( 𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥 ) } |
| 50 |
45 47 49
|
3eqtr4g |
⊢ ( 𝐴 ∈ dom card → ∩ { 𝑦 ∈ On ∣ 𝐴 ≺ 𝑦 } = ∩ { 𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥 } ) |
| 51 |
1 50
|
eqtrd |
⊢ ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) = ∩ { 𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥 } ) |