Step | Hyp | Ref
| Expression |
1 | | tgqioo.1 |
. 2
β’ π = (topGenβ((,) β
(β Γ β))) |
2 | | imassrn 6028 |
. . 3
β’ ((,)
β (β Γ β)) β ran (,) |
3 | | ioof 13373 |
. . . . . 6
β’
(,):(β* Γ β*)βΆπ«
β |
4 | | ffn 6672 |
. . . . . 6
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
5 | 3, 4 | ax-mp 5 |
. . . . 5
β’ (,) Fn
(β* Γ β*) |
6 | | simpll 766 |
. . . . . . . . . 10
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β π₯ β β*) |
7 | | elioo1 13313 |
. . . . . . . . . . . 12
β’ ((π₯ β β*
β§ π¦ β
β*) β (π§ β (π₯(,)π¦) β (π§ β β* β§ π₯ < π§ β§ π§ < π¦))) |
8 | 7 | biimpa 478 |
. . . . . . . . . . 11
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β (π§ β β* β§ π₯ < π§ β§ π§ < π¦)) |
9 | 8 | simp1d 1143 |
. . . . . . . . . 10
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β π§ β β*) |
10 | 8 | simp2d 1144 |
. . . . . . . . . 10
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β π₯ < π§) |
11 | | qbtwnxr 13128 |
. . . . . . . . . 10
β’ ((π₯ β β*
β§ π§ β
β* β§ π₯
< π§) β βπ’ β β (π₯ < π’ β§ π’ < π§)) |
12 | 6, 9, 10, 11 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β βπ’ β β (π₯ < π’ β§ π’ < π§)) |
13 | | simplr 768 |
. . . . . . . . . 10
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β π¦ β β*) |
14 | 8 | simp3d 1145 |
. . . . . . . . . 10
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β π§ < π¦) |
15 | | qbtwnxr 13128 |
. . . . . . . . . 10
β’ ((π§ β β*
β§ π¦ β
β* β§ π§
< π¦) β βπ£ β β (π§ < π£ β§ π£ < π¦)) |
16 | 9, 13, 14, 15 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β βπ£ β β (π§ < π£ β§ π£ < π¦)) |
17 | | reeanv 3216 |
. . . . . . . . . 10
β’
(βπ’ β
β βπ£ β
β ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦)) β (βπ’ β β (π₯ < π’ β§ π’ < π§) β§ βπ£ β β (π§ < π£ β§ π£ < π¦))) |
18 | | df-ov 7364 |
. . . . . . . . . . . . . 14
β’ (π’(,)π£) = ((,)ββ¨π’, π£β©) |
19 | | opelxpi 5674 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β β β§ π£ β β) β
β¨π’, π£β© β (β Γ
β)) |
20 | 19 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β β¨π’, π£β© β (β Γ
β)) |
21 | | ffun 6675 |
. . . . . . . . . . . . . . . . 17
β’
((,):(β* Γ β*)βΆπ«
β β Fun (,)) |
22 | 3, 21 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ Fun
(,) |
23 | | qssre 12892 |
. . . . . . . . . . . . . . . . . . 19
β’ β
β β |
24 | | ressxr 11207 |
. . . . . . . . . . . . . . . . . . 19
β’ β
β β* |
25 | 23, 24 | sstri 3957 |
. . . . . . . . . . . . . . . . . 18
β’ β
β β* |
26 | | xpss12 5652 |
. . . . . . . . . . . . . . . . . 18
β’ ((β
β β* β§ β β β*) β
(β Γ β) β (β* Γ
β*)) |
27 | 25, 25, 26 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
β’ (β
Γ β) β (β* Γ
β*) |
28 | 3 | fdmi 6684 |
. . . . . . . . . . . . . . . . 17
β’ dom (,) =
(β* Γ β*) |
29 | 27, 28 | sseqtrri 3985 |
. . . . . . . . . . . . . . . 16
β’ (β
Γ β) β dom (,) |
30 | | funfvima2 7185 |
. . . . . . . . . . . . . . . 16
β’ ((Fun (,)
β§ (β Γ β) β dom (,)) β (β¨π’, π£β© β (β Γ β)
β ((,)ββ¨π’,
π£β©) β ((,)
β (β Γ β)))) |
31 | 22, 29, 30 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’
(β¨π’, π£β© β (β Γ
β) β ((,)ββ¨π’, π£β©) β ((,) β (β Γ
β))) |
32 | 20, 31 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β ((,)ββ¨π’, π£β©) β ((,) β (β Γ
β))) |
33 | 18, 32 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β (π’(,)π£) β ((,) β (β Γ
β))) |
34 | 9 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π§ β β*) |
35 | | simp3lr 1246 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π’ < π§) |
36 | | simp3rl 1247 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π§ < π£) |
37 | | simp2l 1200 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π’ β β) |
38 | 25, 37 | sselid 3946 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π’ β β*) |
39 | | simp2r 1201 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π£ β β) |
40 | 25, 39 | sselid 3946 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π£ β β*) |
41 | | elioo1 13313 |
. . . . . . . . . . . . . . 15
β’ ((π’ β β*
β§ π£ β
β*) β (π§ β (π’(,)π£) β (π§ β β* β§ π’ < π§ β§ π§ < π£))) |
42 | 38, 40, 41 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β (π§ β (π’(,)π£) β (π§ β β* β§ π’ < π§ β§ π§ < π£))) |
43 | 34, 35, 36, 42 | mpbir3and 1343 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π§ β (π’(,)π£)) |
44 | 6 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π₯ β β*) |
45 | | simp3ll 1245 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π₯ < π’) |
46 | 44, 38, 45 | xrltled 13078 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π₯ β€ π’) |
47 | | iooss1 13308 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β*
β§ π₯ β€ π’) β (π’(,)π£) β (π₯(,)π£)) |
48 | 44, 46, 47 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β (π’(,)π£) β (π₯(,)π£)) |
49 | 13 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π¦ β β*) |
50 | | simp3rr 1248 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π£ < π¦) |
51 | 40, 49, 50 | xrltled 13078 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β π£ β€ π¦) |
52 | | iooss2 13309 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β*
β§ π£ β€ π¦) β (π₯(,)π£) β (π₯(,)π¦)) |
53 | 49, 51, 52 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β (π₯(,)π£) β (π₯(,)π¦)) |
54 | 48, 53 | sstrd 3958 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β (π’(,)π£) β (π₯(,)π¦)) |
55 | | eleq2 2823 |
. . . . . . . . . . . . . . 15
β’ (π€ = (π’(,)π£) β (π§ β π€ β π§ β (π’(,)π£))) |
56 | | sseq1 3973 |
. . . . . . . . . . . . . . 15
β’ (π€ = (π’(,)π£) β (π€ β (π₯(,)π¦) β (π’(,)π£) β (π₯(,)π¦))) |
57 | 55, 56 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π€ = (π’(,)π£) β ((π§ β π€ β§ π€ β (π₯(,)π¦)) β (π§ β (π’(,)π£) β§ (π’(,)π£) β (π₯(,)π¦)))) |
58 | 57 | rspcev 3583 |
. . . . . . . . . . . . 13
β’ (((π’(,)π£) β ((,) β (β Γ
β)) β§ (π§ β
(π’(,)π£) β§ (π’(,)π£) β (π₯(,)π¦))) β βπ€ β ((,) β (β Γ
β))(π§ β π€ β§ π€ β (π₯(,)π¦))) |
59 | 33, 43, 54, 58 | syl12anc 836 |
. . . . . . . . . . . 12
β’ ((((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β§ (π’ β β β§ π£ β β) β§ ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦))) β βπ€ β ((,) β (β Γ
β))(π§ β π€ β§ π€ β (π₯(,)π¦))) |
60 | 59 | 3exp 1120 |
. . . . . . . . . . 11
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β ((π’ β β β§ π£ β β) β (((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦)) β βπ€ β ((,) β (β Γ
β))(π§ β π€ β§ π€ β (π₯(,)π¦))))) |
61 | 60 | rexlimdvv 3201 |
. . . . . . . . . 10
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β (βπ’ β β βπ£ β β ((π₯ < π’ β§ π’ < π§) β§ (π§ < π£ β§ π£ < π¦)) β βπ€ β ((,) β (β Γ
β))(π§ β π€ β§ π€ β (π₯(,)π¦)))) |
62 | 17, 61 | biimtrrid 242 |
. . . . . . . . 9
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β ((βπ’ β β (π₯ < π’ β§ π’ < π§) β§ βπ£ β β (π§ < π£ β§ π£ < π¦)) β βπ€ β ((,) β (β Γ
β))(π§ β π€ β§ π€ β (π₯(,)π¦)))) |
63 | 12, 16, 62 | mp2and 698 |
. . . . . . . 8
β’ (((π₯ β β*
β§ π¦ β
β*) β§ π§ β (π₯(,)π¦)) β βπ€ β ((,) β (β Γ
β))(π§ β π€ β§ π€ β (π₯(,)π¦))) |
64 | 63 | ralrimiva 3140 |
. . . . . . 7
β’ ((π₯ β β*
β§ π¦ β
β*) β βπ§ β (π₯(,)π¦)βπ€ β ((,) β (β Γ
β))(π§ β π€ β§ π€ β (π₯(,)π¦))) |
65 | | qtopbas 24146 |
. . . . . . . 8
β’ ((,)
β (β Γ β)) β TopBases |
66 | | eltg2b 22332 |
. . . . . . . 8
β’ (((,)
β (β Γ β)) β TopBases β ((π₯(,)π¦) β (topGenβ((,) β (β
Γ β))) β βπ§ β (π₯(,)π¦)βπ€ β ((,) β (β Γ
β))(π§ β π€ β§ π€ β (π₯(,)π¦)))) |
67 | 65, 66 | ax-mp 5 |
. . . . . . 7
β’ ((π₯(,)π¦) β (topGenβ((,) β (β
Γ β))) β βπ§ β (π₯(,)π¦)βπ€ β ((,) β (β Γ
β))(π§ β π€ β§ π€ β (π₯(,)π¦))) |
68 | 64, 67 | sylibr 233 |
. . . . . 6
β’ ((π₯ β β*
β§ π¦ β
β*) β (π₯(,)π¦) β (topGenβ((,) β (β
Γ β)))) |
69 | 68 | rgen2 3191 |
. . . . 5
β’
βπ₯ β
β* βπ¦ β β* (π₯(,)π¦) β (topGenβ((,) β (β
Γ β))) |
70 | | ffnov 7487 |
. . . . 5
β’
((,):(β* Γ
β*)βΆ(topGenβ((,) β (β Γ
β))) β ((,) Fn (β* Γ β*)
β§ βπ₯ β
β* βπ¦ β β* (π₯(,)π¦) β (topGenβ((,) β (β
Γ β))))) |
71 | 5, 69, 70 | mpbir2an 710 |
. . . 4
β’
(,):(β* Γ
β*)βΆ(topGenβ((,) β (β Γ
β))) |
72 | | frn 6679 |
. . . 4
β’
((,):(β* Γ
β*)βΆ(topGenβ((,) β (β Γ
β))) β ran (,) β (topGenβ((,) β (β Γ
β)))) |
73 | 71, 72 | ax-mp 5 |
. . 3
β’ ran (,)
β (topGenβ((,) β (β Γ β))) |
74 | | 2basgen 22363 |
. . 3
β’ ((((,)
β (β Γ β)) β ran (,) β§ ran (,) β
(topGenβ((,) β (β Γ β)))) β
(topGenβ((,) β (β Γ β))) = (topGenβran
(,))) |
75 | 2, 73, 74 | mp2an 691 |
. 2
β’
(topGenβ((,) β (β Γ β))) =
(topGenβran (,)) |
76 | 1, 75 | eqtr2i 2762 |
1
β’
(topGenβran (,)) = π |