Step | Hyp | Ref
| Expression |
1 | | eqid 2740 |
. . . . . 6
⊢
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} = {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
2 | | eqid 2740 |
. . . . . 6
⊢
{〈𝑠, 𝑡〉 ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)} = {〈𝑠, 𝑡〉 ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)} |
3 | 1, 2 | hartogslem1 9279 |
. . . . 5
⊢ (dom
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝑋 × 𝑋) ∧ Fun {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∧ (𝑋 ∈ 𝑉 → ran {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} = {𝑥 ∈ On ∣ 𝑥 ≼ 𝑋})) |
4 | 3 | simp2i 1139 |
. . . 4
⊢ Fun
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
5 | 3 | simp1i 1138 |
. . . . 5
⊢ dom
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝑋 × 𝑋) |
6 | | sqxpexg 7599 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → (𝑋 × 𝑋) ∈ V) |
7 | 6 | pwexd 5306 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝒫 (𝑋 × 𝑋) ∈ V) |
8 | | ssexg 5251 |
. . . . 5
⊢ ((dom
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝑋 × 𝑋) ∧ 𝒫 (𝑋 × 𝑋) ∈ V) → dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∈ V) |
9 | 5, 7, 8 | sylancr 587 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∈ V) |
10 | | funex 7092 |
. . . 4
⊢ ((Fun
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∧ dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∈ V) → {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∈ V) |
11 | 4, 9, 10 | sylancr 587 |
. . 3
⊢ (𝑋 ∈ 𝑉 → {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∈ V) |
12 | | funfn 6462 |
. . . . . 6
⊢ (Fun
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ↔ {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} Fn dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}) |
13 | 4, 12 | mpbi 229 |
. . . . 5
⊢
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} Fn dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} Fn dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}) |
15 | 3 | simp3i 1140 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → ran {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} = {𝑥 ∈ On ∣ 𝑥 ≼ 𝑋}) |
16 | | harval 9297 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) = {𝑥 ∈ On ∣ 𝑥 ≼ 𝑋}) |
17 | 15, 16 | eqtr4d 2783 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → ran {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} = (har‘𝑋)) |
18 | | df-fo 6438 |
. . . 4
⊢
({〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}:dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}–onto→(har‘𝑋) ↔ ({〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} Fn dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∧ ran {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} = (har‘𝑋))) |
19 | 14, 17, 18 | sylanbrc 583 |
. . 3
⊢ (𝑋 ∈ 𝑉 → {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}:dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}–onto→(har‘𝑋)) |
20 | | fowdom 9308 |
. . 3
⊢
(({〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∈ V ∧ {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}:dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}–onto→(har‘𝑋)) → (har‘𝑋) ≼* dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}) |
21 | 11, 19, 20 | syl2anc 584 |
. 2
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) ≼* dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}) |
22 | | ssdomg 8769 |
. . . 4
⊢
(𝒫 (𝑋
× 𝑋) ∈ V →
(dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝑋 × 𝑋) → dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ≼ 𝒫 (𝑋 × 𝑋))) |
23 | 7, 5, 22 | mpisyl 21 |
. . 3
⊢ (𝑋 ∈ 𝑉 → dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ≼ 𝒫 (𝑋 × 𝑋)) |
24 | | domwdom 9311 |
. . 3
⊢ (dom
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ≼ 𝒫 (𝑋 × 𝑋) → dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ≼* 𝒫 (𝑋 × 𝑋)) |
25 | 23, 24 | syl 17 |
. 2
⊢ (𝑋 ∈ 𝑉 → dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ≼* 𝒫 (𝑋 × 𝑋)) |
26 | | wdomtr 9312 |
. 2
⊢
(((har‘𝑋)
≼* dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∧ dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ≼* 𝒫 (𝑋 × 𝑋)) → (har‘𝑋) ≼* 𝒫 (𝑋 × 𝑋)) |
27 | 21, 25, 26 | syl2anc 584 |
1
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) ≼* 𝒫 (𝑋 × 𝑋)) |