Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 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 2733 |
. . . . . 6
β’
{β¨π , π‘β© β£ βπ€ β π¦ βπ§ β π¦ ((π = (πβπ€) β§ π‘ = (πβπ§)) β§ π€ E π§)} = {β¨π , π‘β© β£ βπ€ β π¦ βπ§ β π¦ ((π = (πβπ€) β§ π‘ = (πβπ§)) β§ π€ E π§)} |
3 | 1, 2 | hartogslem1 9486 |
. . . . 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 1141 |
. . . 4
β’ Fun
{β¨π, π¦β© β£ (((dom π β π β§ ( I βΎ dom π) β π β§ π β (dom π Γ dom π)) β§ (π β I ) We dom π) β§ π¦ = dom OrdIso((π β I ), dom π))} |
5 | 3 | simp1i 1140 |
. . . . 5
β’ dom
{β¨π, π¦β© β£ (((dom π β π β§ ( I βΎ dom π) β π β§ π β (dom π Γ dom π)) β§ (π β I ) We dom π) β§ π¦ = dom OrdIso((π β I ), dom π))} β π« (π Γ π) |
6 | | sqxpexg 7693 |
. . . . . 6
β’ (π β π β (π Γ π) β V) |
7 | 6 | pwexd 5338 |
. . . . 5
β’ (π β π β π« (π Γ π) β V) |
8 | | ssexg 5284 |
. . . . 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 588 |
. . . 4
β’ (π β π β dom {β¨π, π¦β© β£ (((dom π β π β§ ( I βΎ dom π) β π β§ π β (dom π Γ dom π)) β§ (π β I ) We dom π) β§ π¦ = dom OrdIso((π β I ), dom π))} β V) |
10 | | funex 7173 |
. . . 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 588 |
. . 3
β’ (π β π β {β¨π, π¦β© β£ (((dom π β π β§ ( I βΎ dom π) β π β§ π β (dom π Γ dom π)) β§ (π β I ) We dom π) β§ π¦ = dom OrdIso((π β I ), dom π))} β V) |
12 | | funfn 6535 |
. . . . . 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 1142 |
. . . . 5
β’ (π β π β ran {β¨π, π¦β© β£ (((dom π β π β§ ( I βΎ dom π) β π β§ π β (dom π Γ dom π)) β§ (π β I ) We dom π) β§ π¦ = dom OrdIso((π β I ), dom π))} = {π₯ β On β£ π₯ βΌ π}) |
16 | | harval 9504 |
. . . . 5
β’ (π β π β (harβπ) = {π₯ β On β£ π₯ βΌ π}) |
17 | 15, 16 | eqtr4d 2776 |
. . . 4
β’ (π β π β ran {β¨π, π¦β© β£ (((dom π β π β§ ( I βΎ dom π) β π β§ π β (dom π Γ dom π)) β§ (π β I ) We dom π) β§ π¦ = dom OrdIso((π β I ), dom π))} = (harβπ)) |
18 | | df-fo 6506 |
. . . 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 584 |
. . 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 9515 |
. . 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 585 |
. 2
β’ (π β π β (harβπ) βΌ* dom {β¨π, π¦β© β£ (((dom π β π β§ ( I βΎ dom π) β π β§ π β (dom π Γ dom π)) β§ (π β I ) We dom π) β§ π¦ = dom OrdIso((π β I ), dom π))}) |
22 | | ssdomg 8946 |
. . . 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 9518 |
. . 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 9519 |
. 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 585 |
1
β’ (π β π β (harβπ) βΌ* π« (π Γ π)) |