Step |
Hyp |
Ref |
Expression |
1 |
|
hartogslem.2 |
⊢ 𝐹 = { 〈 𝑟 , 𝑦 〉 ∣ ( ( ( dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ 𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) } |
2 |
|
hartogslem.3 |
⊢ 𝑅 = { 〈 𝑠 , 𝑡 〉 ∣ ∃ 𝑤 ∈ 𝑦 ∃ 𝑧 ∈ 𝑦 ( ( 𝑠 = ( 𝑓 ‘ 𝑤 ) ∧ 𝑡 = ( 𝑓 ‘ 𝑧 ) ) ∧ 𝑤 E 𝑧 ) } |
3 |
1 2
|
hartogslem1 |
⊢ ( dom 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐴 ) ∧ Fun 𝐹 ∧ ( 𝐴 ∈ 𝑉 → ran 𝐹 = { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) ) |
4 |
3
|
simp3i |
⊢ ( 𝐴 ∈ 𝑉 → ran 𝐹 = { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ) |
5 |
3
|
simp2i |
⊢ Fun 𝐹 |
6 |
3
|
simp1i |
⊢ dom 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐴 ) |
7 |
|
sqxpexg |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × 𝐴 ) ∈ V ) |
8 |
7
|
pwexd |
⊢ ( 𝐴 ∈ 𝑉 → 𝒫 ( 𝐴 × 𝐴 ) ∈ V ) |
9 |
|
ssexg |
⊢ ( ( dom 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐴 ) ∧ 𝒫 ( 𝐴 × 𝐴 ) ∈ V ) → dom 𝐹 ∈ V ) |
10 |
6 8 9
|
sylancr |
⊢ ( 𝐴 ∈ 𝑉 → dom 𝐹 ∈ V ) |
11 |
|
funex |
⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ∈ V ) → 𝐹 ∈ V ) |
12 |
5 10 11
|
sylancr |
⊢ ( 𝐴 ∈ 𝑉 → 𝐹 ∈ V ) |
13 |
|
rnexg |
⊢ ( 𝐹 ∈ V → ran 𝐹 ∈ V ) |
14 |
12 13
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → ran 𝐹 ∈ V ) |
15 |
4 14
|
eqeltrrd |
⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ On ∣ 𝑥 ≼ 𝐴 } ∈ V ) |