Step |
Hyp |
Ref |
Expression |
1 |
|
elfvex |
⊢ ( 𝑌 ∈ ( har ‘ 𝑋 ) → 𝑋 ∈ V ) |
2 |
|
reldom |
⊢ Rel ≼ |
3 |
2
|
brrelex2i |
⊢ ( 𝑌 ≼ 𝑋 → 𝑋 ∈ V ) |
4 |
3
|
adantl |
⊢ ( ( 𝑌 ∈ On ∧ 𝑌 ≼ 𝑋 ) → 𝑋 ∈ V ) |
5 |
|
harval |
⊢ ( 𝑋 ∈ V → ( har ‘ 𝑋 ) = { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑋 } ) |
6 |
5
|
eleq2d |
⊢ ( 𝑋 ∈ V → ( 𝑌 ∈ ( har ‘ 𝑋 ) ↔ 𝑌 ∈ { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑋 } ) ) |
7 |
|
breq1 |
⊢ ( 𝑦 = 𝑌 → ( 𝑦 ≼ 𝑋 ↔ 𝑌 ≼ 𝑋 ) ) |
8 |
7
|
elrab |
⊢ ( 𝑌 ∈ { 𝑦 ∈ On ∣ 𝑦 ≼ 𝑋 } ↔ ( 𝑌 ∈ On ∧ 𝑌 ≼ 𝑋 ) ) |
9 |
6 8
|
bitrdi |
⊢ ( 𝑋 ∈ V → ( 𝑌 ∈ ( har ‘ 𝑋 ) ↔ ( 𝑌 ∈ On ∧ 𝑌 ≼ 𝑋 ) ) ) |
10 |
1 4 9
|
pm5.21nii |
⊢ ( 𝑌 ∈ ( har ‘ 𝑋 ) ↔ ( 𝑌 ∈ On ∧ 𝑌 ≼ 𝑋 ) ) |