Step | Hyp | Ref
| Expression |
1 | | harval2 9613 |
. 2
⊢ (𝐴 ∈ dom card →
(har‘𝐴) = ∩ {𝑦
∈ On ∣ 𝐴 ≺
𝑦}) |
2 | | vex 3412 |
. . . . . 6
⊢ 𝑥 ∈ V |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ dom card → 𝑥 ∈ V) |
4 | | elrncard 40827 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran card ↔ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 ¬ 𝑦 ≈ 𝑥)) |
5 | 4 | simplbi 501 |
. . . . . . . 8
⊢ (𝑥 ∈ ran card → 𝑥 ∈ On) |
6 | 5 | anim1i 618 |
. . . . . . 7
⊢ ((𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥) → (𝑥 ∈ On ∧ 𝐴 ≺ 𝑥)) |
7 | | eleq1 2825 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑦 ∈ On ↔ 𝑥 ∈ On)) |
8 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝐴 ≺ 𝑦 ↔ 𝐴 ≺ 𝑥)) |
9 | 7, 8 | anbi12d 634 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((𝑦 ∈ On ∧ 𝐴 ≺ 𝑦) ↔ (𝑥 ∈ On ∧ 𝐴 ≺ 𝑥))) |
10 | 6, 9 | syl5ibr 249 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥) → (𝑦 ∈ On ∧ 𝐴 ≺ 𝑦))) |
11 | 10 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ 𝑦 = 𝑥) → ((𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥) → (𝑦 ∈ On ∧ 𝐴 ≺ 𝑦))) |
12 | | ssidd 3924 |
. . . . 5
⊢ (𝐴 ∈ dom card → 𝑥 ⊆ 𝑥) |
13 | 3, 11, 12 | intabssd 40811 |
. . . 4
⊢ (𝐴 ∈ dom card → ∩ {𝑦
∣ (𝑦 ∈ On ∧
𝐴 ≺ 𝑦)} ⊆ ∩ {𝑥
∣ (𝑥 ∈ ran card
∧ 𝐴 ≺ 𝑥)}) |
14 | | vex 3412 |
. . . . . . 7
⊢ 𝑦 ∈ V |
15 | 14 | inex1 5210 |
. . . . . 6
⊢ (𝑦 ∩ (card‘𝑦)) ∈ V |
16 | 15 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ dom card → (𝑦 ∩ (card‘𝑦)) ∈ V) |
17 | | oncardid 9572 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ On →
(card‘𝑦) ≈
𝑦) |
18 | 17 | ensymd 8679 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → 𝑦 ≈ (card‘𝑦)) |
19 | | sdomentr 8780 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≺ 𝑦 ∧ 𝑦 ≈ (card‘𝑦)) → 𝐴 ≺ (card‘𝑦)) |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → ((𝐴 ≺ 𝑦 ∧ 𝑦 ≈ (card‘𝑦)) → 𝐴 ≺ (card‘𝑦))) |
21 | 18, 20 | mpan2d 694 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On → (𝐴 ≺ 𝑦 → 𝐴 ≺ (card‘𝑦))) |
22 | | df-card 9555 |
. . . . . . . . . . . 12
⊢ card =
(𝑥 ∈ V ↦ ∩ {𝑦
∈ On ∣ 𝑦 ≈
𝑥}) |
23 | 22 | funmpt2 6419 |
. . . . . . . . . . 11
⊢ Fun
card |
24 | | onenon 9565 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → 𝑦 ∈ dom
card) |
25 | | fvelrn 6897 |
. . . . . . . . . . 11
⊢ ((Fun
card ∧ 𝑦 ∈ dom
card) → (card‘𝑦)
∈ ran card) |
26 | 23, 24, 25 | sylancr 590 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On →
(card‘𝑦) ∈ ran
card) |
27 | 21, 26 | jctild 529 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → (𝐴 ≺ 𝑦 → ((card‘𝑦) ∈ ran card ∧ 𝐴 ≺ (card‘𝑦)))) |
28 | 27 | adantl 485 |
. . . . . . . 8
⊢ ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → (𝐴 ≺ 𝑦 → ((card‘𝑦) ∈ ran card ∧ 𝐴 ≺ (card‘𝑦)))) |
29 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → 𝑥 = (𝑦 ∩ (card‘𝑦))) |
30 | | cardonle 9573 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ On →
(card‘𝑦) ⊆
𝑦) |
31 | 30 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → (card‘𝑦) ⊆ 𝑦) |
32 | | sseqin2 4130 |
. . . . . . . . . . 11
⊢
((card‘𝑦)
⊆ 𝑦 ↔ (𝑦 ∩ (card‘𝑦)) = (card‘𝑦)) |
33 | 31, 32 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → (𝑦 ∩ (card‘𝑦)) = (card‘𝑦)) |
34 | 29, 33 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → 𝑥 = (card‘𝑦)) |
35 | | eleq1 2825 |
. . . . . . . . . 10
⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ ran card ↔ (card‘𝑦) ∈ ran
card)) |
36 | | breq2 5057 |
. . . . . . . . . 10
⊢ (𝑥 = (card‘𝑦) → (𝐴 ≺ 𝑥 ↔ 𝐴 ≺ (card‘𝑦))) |
37 | 35, 36 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑥 = (card‘𝑦) → ((𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥) ↔ ((card‘𝑦) ∈ ran card ∧ 𝐴 ≺ (card‘𝑦)))) |
38 | 34, 37 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → ((𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥) ↔ ((card‘𝑦) ∈ ran card ∧ 𝐴 ≺ (card‘𝑦)))) |
39 | 28, 38 | sylibrd 262 |
. . . . . . 7
⊢ ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → (𝐴 ≺ 𝑦 → (𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥))) |
40 | 39 | expimpd 457 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∩ (card‘𝑦)) → ((𝑦 ∈ On ∧ 𝐴 ≺ 𝑦) → (𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥))) |
41 | 40 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ 𝑥 = (𝑦 ∩ (card‘𝑦))) → ((𝑦 ∈ On ∧ 𝐴 ≺ 𝑦) → (𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥))) |
42 | | inss1 4143 |
. . . . . 6
⊢ (𝑦 ∩ (card‘𝑦)) ⊆ 𝑦 |
43 | 42 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ dom card → (𝑦 ∩ (card‘𝑦)) ⊆ 𝑦) |
44 | 16, 41, 43 | intabssd 40811 |
. . . 4
⊢ (𝐴 ∈ dom card → ∩ {𝑥
∣ (𝑥 ∈ ran card
∧ 𝐴 ≺ 𝑥)} ⊆ ∩ {𝑦
∣ (𝑦 ∈ On ∧
𝐴 ≺ 𝑦)}) |
45 | 13, 44 | eqssd 3918 |
. . 3
⊢ (𝐴 ∈ dom card → ∩ {𝑦
∣ (𝑦 ∈ On ∧
𝐴 ≺ 𝑦)} = ∩ {𝑥
∣ (𝑥 ∈ ran card
∧ 𝐴 ≺ 𝑥)}) |
46 | | df-rab 3070 |
. . . 4
⊢ {𝑦 ∈ On ∣ 𝐴 ≺ 𝑦} = {𝑦 ∣ (𝑦 ∈ On ∧ 𝐴 ≺ 𝑦)} |
47 | 46 | inteqi 4863 |
. . 3
⊢ ∩ {𝑦
∈ On ∣ 𝐴 ≺
𝑦} = ∩ {𝑦
∣ (𝑦 ∈ On ∧
𝐴 ≺ 𝑦)} |
48 | | df-rab 3070 |
. . . 4
⊢ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥} = {𝑥 ∣ (𝑥 ∈ ran card ∧ 𝐴 ≺ 𝑥)} |
49 | 48 | inteqi 4863 |
. . 3
⊢ ∩ {𝑥
∈ ran card ∣ 𝐴
≺ 𝑥} = ∩ {𝑥
∣ (𝑥 ∈ ran card
∧ 𝐴 ≺ 𝑥)} |
50 | 45, 47, 49 | 3eqtr4g 2803 |
. 2
⊢ (𝐴 ∈ dom card → ∩ {𝑦
∈ On ∣ 𝐴 ≺
𝑦} = ∩ {𝑥
∈ ran card ∣ 𝐴
≺ 𝑥}) |
51 | 1, 50 | eqtrd 2777 |
1
⊢ (𝐴 ∈ dom card →
(har‘𝐴) = ∩ {𝑥
∈ ran card ∣ 𝐴
≺ 𝑥}) |