Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 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 2610 |
. . . . . 6
⊢
{〈𝑠, 𝑡〉 ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)} = {〈𝑠, 𝑡〉 ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)} |
3 | 1, 2 | hartogslem1 8330 |
. . . . 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 1064 |
. . . 4
⊢ Fun
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} |
5 | 3 | simp1i 1063 |
. . . . 5
⊢ dom
{〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ⊆ 𝒫 (𝑋 × 𝑋) |
6 | | sqxpexg 6861 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → (𝑋 × 𝑋) ∈ V) |
7 | | pwexg 4776 |
. . . . . 6
⊢ ((𝑋 × 𝑋) ∈ V → 𝒫 (𝑋 × 𝑋) ∈ V) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝒫 (𝑋 × 𝑋) ∈ V) |
9 | | ssexg 4732 |
. . . . 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) |
10 | 5, 8, 9 | sylancr 694 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∈ V) |
11 | | funex 6387 |
. . . 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) |
12 | 4, 10, 11 | sylancr 694 |
. . 3
⊢ (𝑋 ∈ 𝑉 → {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ∈ V) |
13 | | funfn 5833 |
. . . . . 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 𝑟))}) |
14 | 4, 13 | mpbi 219 |
. . . . 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 𝑟))} |
15 | 14 | 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 𝑟))}) |
16 | 3 | simp3i 1065 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → ran {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} = {𝑥 ∈ On ∣ 𝑥 ≼ 𝑋}) |
17 | | harval 8350 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) = {𝑥 ∈ On ∣ 𝑥 ≼ 𝑋}) |
18 | 16, 17 | eqtr4d 2647 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → ran {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} = (har‘𝑋)) |
19 | | df-fo 5810 |
. . . 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‘𝑋))) |
20 | 15, 18, 19 | sylanbrc 695 |
. . 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‘𝑋)) |
21 | | fowdom 8359 |
. . 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 𝑟))}) |
22 | 12, 20, 21 | syl2anc 691 |
. 2
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) ≼* dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}) |
23 | | ssdomg 7887 |
. . . 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 𝑟))} ≼ 𝒫 (𝑋 × 𝑋))) |
24 | 8, 5, 23 | mpisyl 21 |
. . 3
⊢ (𝑋 ∈ 𝑉 → dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ≼ 𝒫 (𝑋 × 𝑋)) |
25 | | domwdom 8362 |
. . 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 𝑟))} ≼* 𝒫 (𝑋 × 𝑋)) |
26 | 24, 25 | syl 17 |
. 2
⊢ (𝑋 ∈ 𝑉 → dom {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝑋 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} ≼* 𝒫 (𝑋 × 𝑋)) |
27 | | wdomtr 8363 |
. 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‘𝑋) ≼* 𝒫 (𝑋 × 𝑋)) |
28 | 22, 26, 27 | syl2anc 691 |
1
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) ≼* 𝒫 (𝑋 × 𝑋)) |