Step | Hyp | Ref
| Expression |
1 | | dya2iocnrect.1 |
. . . . . 6
β’ π΅ = ran (π β ran (,), π β ran (,) β¦ (π Γ π)) |
2 | 1 | eleq2i 2824 |
. . . . 5
β’ (π΄ β π΅ β π΄ β ran (π β ran (,), π β ran (,) β¦ (π Γ π))) |
3 | | eqid 2731 |
. . . . . 6
β’ (π β ran (,), π β ran (,) β¦ (π Γ π)) = (π β ran (,), π β ran (,) β¦ (π Γ π)) |
4 | | vex 3477 |
. . . . . . 7
β’ π β V |
5 | | vex 3477 |
. . . . . . 7
β’ π β V |
6 | 4, 5 | xpex 7744 |
. . . . . 6
β’ (π Γ π) β V |
7 | 3, 6 | elrnmpo 7548 |
. . . . 5
β’ (π΄ β ran (π β ran (,), π β ran (,) β¦ (π Γ π)) β βπ β ran (,)βπ β ran (,)π΄ = (π Γ π)) |
8 | 2, 7 | sylbb 218 |
. . . 4
β’ (π΄ β π΅ β βπ β ran (,)βπ β ran (,)π΄ = (π Γ π)) |
9 | 8 | 3ad2ant2 1133 |
. . 3
β’ ((π β (β Γ
β) β§ π΄ β
π΅ β§ π β π΄) β βπ β ran (,)βπ β ran (,)π΄ = (π Γ π)) |
10 | | simp1 1135 |
. . 3
β’ ((π β (β Γ
β) β§ π΄ β
π΅ β§ π β π΄) β π β (β Γ
β)) |
11 | | simp3 1137 |
. . 3
β’ ((π β (β Γ
β) β§ π΄ β
π΅ β§ π β π΄) β π β π΄) |
12 | 9, 10, 11 | jca32 515 |
. 2
β’ ((π β (β Γ
β) β§ π΄ β
π΅ β§ π β π΄) β (βπ β ran (,)βπ β ran (,)π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄))) |
13 | | r19.41vv 3223 |
. . 3
β’
(βπ β ran
(,)βπ β ran
(,)(π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄)) β (βπ β ran (,)βπ β ran (,)π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄))) |
14 | 13 | biimpri 227 |
. 2
β’
((βπ β
ran (,)βπ β ran
(,)π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄)) β βπ β ran (,)βπ β ran (,)(π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄))) |
15 | | simprl 768 |
. . . . . 6
β’ ((π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄)) β π β (β Γ
β)) |
16 | | simpl 482 |
. . . . . 6
β’ ((π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄)) β π΄ = (π Γ π)) |
17 | | simprr 770 |
. . . . . . 7
β’ ((π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄)) β π β π΄) |
18 | 17, 16 | eleqtrd 2834 |
. . . . . 6
β’ ((π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄)) β π β (π Γ π)) |
19 | 15, 16, 18 | 3jca 1127 |
. . . . 5
β’ ((π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄)) β (π β (β Γ β) β§
π΄ = (π Γ π) β§ π β (π Γ π))) |
20 | | simpr 484 |
. . . . . 6
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β (π β (β Γ β) β§
π΄ = (π Γ π) β§ π β (π Γ π))) |
21 | | xp1st 8011 |
. . . . . . . . . 10
β’ (π β (β Γ
β) β (1st βπ) β β) |
22 | 21 | 3ad2ant1 1132 |
. . . . . . . . 9
β’ ((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β (1st βπ) β
β) |
23 | 22 | adantl 481 |
. . . . . . . 8
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β (1st βπ) β
β) |
24 | | simpll 764 |
. . . . . . . 8
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β π β ran (,)) |
25 | | xp1st 8011 |
. . . . . . . . . 10
β’ (π β (π Γ π) β (1st βπ) β π) |
26 | 25 | 3ad2ant3 1134 |
. . . . . . . . 9
β’ ((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β (1st βπ) β π) |
27 | 26 | adantl 481 |
. . . . . . . 8
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β (1st βπ) β π) |
28 | | sxbrsiga.0 |
. . . . . . . . 9
β’ π½ = (topGenβran
(,)) |
29 | | dya2ioc.1 |
. . . . . . . . 9
β’ πΌ = (π₯ β β€, π β β€ β¦ ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) |
30 | 28, 29 | dya2icoseg2 33576 |
. . . . . . . 8
β’
(((1st βπ) β β β§ π β ran (,) β§ (1st
βπ) β π) β βπ β ran πΌ((1st βπ) β π β§ π β π)) |
31 | 23, 24, 27, 30 | syl3anc 1370 |
. . . . . . 7
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β βπ β ran πΌ((1st βπ) β π β§ π β π)) |
32 | | xp2nd 8012 |
. . . . . . . . . 10
β’ (π β (β Γ
β) β (2nd βπ) β β) |
33 | 32 | 3ad2ant1 1132 |
. . . . . . . . 9
β’ ((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β (2nd βπ) β
β) |
34 | 33 | adantl 481 |
. . . . . . . 8
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β (2nd βπ) β
β) |
35 | | simplr 766 |
. . . . . . . 8
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β π β ran (,)) |
36 | | xp2nd 8012 |
. . . . . . . . . 10
β’ (π β (π Γ π) β (2nd βπ) β π) |
37 | 36 | 3ad2ant3 1134 |
. . . . . . . . 9
β’ ((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β (2nd βπ) β π) |
38 | 37 | adantl 481 |
. . . . . . . 8
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β (2nd βπ) β π) |
39 | 28, 29 | dya2icoseg2 33576 |
. . . . . . . 8
β’
(((2nd βπ) β β β§ π β ran (,) β§ (2nd
βπ) β π) β βπ‘ β ran πΌ((2nd βπ) β π‘ β§ π‘ β π)) |
40 | 34, 35, 38, 39 | syl3anc 1370 |
. . . . . . 7
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β βπ‘ β ran πΌ((2nd βπ) β π‘ β§ π‘ β π)) |
41 | | reeanv 3225 |
. . . . . . 7
β’
(βπ β ran
πΌβπ‘ β ran πΌ(((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)) β (βπ β ran πΌ((1st βπ) β π β§ π β π) β§ βπ‘ β ran πΌ((2nd βπ) β π‘ β§ π‘ β π))) |
42 | 31, 40, 41 | sylanbrc 582 |
. . . . . 6
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β βπ β ran πΌβπ‘ β ran πΌ(((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π))) |
43 | | eqid 2731 |
. . . . . . . . . . . 12
β’ (π Γ π‘) = (π Γ π‘) |
44 | | xpeq1 5690 |
. . . . . . . . . . . . . 14
β’ (π’ = π β (π’ Γ π£) = (π Γ π£)) |
45 | 44 | eqeq2d 2742 |
. . . . . . . . . . . . 13
β’ (π’ = π β ((π Γ π‘) = (π’ Γ π£) β (π Γ π‘) = (π Γ π£))) |
46 | | xpeq2 5697 |
. . . . . . . . . . . . . 14
β’ (π£ = π‘ β (π Γ π£) = (π Γ π‘)) |
47 | 46 | eqeq2d 2742 |
. . . . . . . . . . . . 13
β’ (π£ = π‘ β ((π Γ π‘) = (π Γ π£) β (π Γ π‘) = (π Γ π‘))) |
48 | 45, 47 | rspc2ev 3624 |
. . . . . . . . . . . 12
β’ ((π β ran πΌ β§ π‘ β ran πΌ β§ (π Γ π‘) = (π Γ π‘)) β βπ’ β ran πΌβπ£ β ran πΌ(π Γ π‘) = (π’ Γ π£)) |
49 | 43, 48 | mp3an3 1449 |
. . . . . . . . . . 11
β’ ((π β ran πΌ β§ π‘ β ran πΌ) β βπ’ β ran πΌβπ£ β ran πΌ(π Γ π‘) = (π’ Γ π£)) |
50 | | dya2ioc.2 |
. . . . . . . . . . . 12
β’ π
= (π’ β ran πΌ, π£ β ran πΌ β¦ (π’ Γ π£)) |
51 | | vex 3477 |
. . . . . . . . . . . . 13
β’ π’ β V |
52 | | vex 3477 |
. . . . . . . . . . . . 13
β’ π£ β V |
53 | 51, 52 | xpex 7744 |
. . . . . . . . . . . 12
β’ (π’ Γ π£) β V |
54 | 50, 53 | elrnmpo 7548 |
. . . . . . . . . . 11
β’ ((π Γ π‘) β ran π
β βπ’ β ran πΌβπ£ β ran πΌ(π Γ π‘) = (π’ Γ π£)) |
55 | 49, 54 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β ran πΌ β§ π‘ β ran πΌ) β (π Γ π‘) β ran π
) |
56 | 55 | ad2antrl 725 |
. . . . . . . . 9
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β (π Γ π‘) β ran π
) |
57 | | xpss 5692 |
. . . . . . . . . . 11
β’ (β
Γ β) β (V Γ V) |
58 | | simpl1 1190 |
. . . . . . . . . . 11
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β π β (β Γ
β)) |
59 | 57, 58 | sselid 3980 |
. . . . . . . . . 10
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β π β (V Γ V)) |
60 | | simprrl 778 |
. . . . . . . . . . 11
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β ((1st βπ) β π β§ π β π)) |
61 | 60 | simpld 494 |
. . . . . . . . . 10
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β (1st βπ) β π ) |
62 | | simprrr 779 |
. . . . . . . . . . 11
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β ((2nd βπ) β π‘ β§ π‘ β π)) |
63 | 62 | simpld 494 |
. . . . . . . . . 10
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β (2nd βπ) β π‘) |
64 | | elxp7 8014 |
. . . . . . . . . . 11
β’ (π β (π Γ π‘) β (π β (V Γ V) β§ ((1st
βπ) β π β§ (2nd
βπ) β π‘))) |
65 | 64 | biimpri 227 |
. . . . . . . . . 10
β’ ((π β (V Γ V) β§
((1st βπ)
β π β§
(2nd βπ)
β π‘)) β π β (π Γ π‘)) |
66 | 59, 61, 63, 65 | syl12anc 834 |
. . . . . . . . 9
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β π β (π Γ π‘)) |
67 | 60 | simprd 495 |
. . . . . . . . . . 11
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β π β π) |
68 | 62 | simprd 495 |
. . . . . . . . . . 11
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β π‘ β π) |
69 | | xpss12 5691 |
. . . . . . . . . . 11
β’ ((π β π β§ π‘ β π) β (π Γ π‘) β (π Γ π)) |
70 | 67, 68, 69 | syl2anc 583 |
. . . . . . . . . 10
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β (π Γ π‘) β (π Γ π)) |
71 | | simpl2 1191 |
. . . . . . . . . 10
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β π΄ = (π Γ π)) |
72 | 70, 71 | sseqtrrd 4023 |
. . . . . . . . 9
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β (π Γ π‘) β π΄) |
73 | | eleq2 2821 |
. . . . . . . . . . 11
β’ (π = (π Γ π‘) β (π β π β π β (π Γ π‘))) |
74 | | sseq1 4007 |
. . . . . . . . . . 11
β’ (π = (π Γ π‘) β (π β π΄ β (π Γ π‘) β π΄)) |
75 | 73, 74 | anbi12d 630 |
. . . . . . . . . 10
β’ (π = (π Γ π‘) β ((π β π β§ π β π΄) β (π β (π Γ π‘) β§ (π Γ π‘) β π΄))) |
76 | 75 | rspcev 3612 |
. . . . . . . . 9
β’ (((π Γ π‘) β ran π
β§ (π β (π Γ π‘) β§ (π Γ π‘) β π΄)) β βπ β ran π
(π β π β§ π β π΄)) |
77 | 56, 66, 72, 76 | syl12anc 834 |
. . . . . . . 8
β’ (((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β§ ((π β ran πΌ β§ π‘ β ran πΌ) β§ (((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)))) β βπ β ran π
(π β π β§ π β π΄)) |
78 | 77 | exp32 420 |
. . . . . . 7
β’ ((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β ((π β ran πΌ β§ π‘ β ran πΌ) β ((((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)) β βπ β ran π
(π β π β§ π β π΄)))) |
79 | 78 | rexlimdvv 3209 |
. . . . . 6
β’ ((π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π)) β (βπ β ran πΌβπ‘ β ran πΌ(((1st βπ) β π β§ π β π) β§ ((2nd βπ) β π‘ β§ π‘ β π)) β βπ β ran π
(π β π β§ π β π΄))) |
80 | 20, 42, 79 | sylc 65 |
. . . . 5
β’ (((π β ran (,) β§ π β ran (,)) β§ (π β (β Γ
β) β§ π΄ = (π Γ π) β§ π β (π Γ π))) β βπ β ran π
(π β π β§ π β π΄)) |
81 | 19, 80 | sylan2 592 |
. . . 4
β’ (((π β ran (,) β§ π β ran (,)) β§ (π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄))) β βπ β ran π
(π β π β§ π β π΄)) |
82 | 81 | ex 412 |
. . 3
β’ ((π β ran (,) β§ π β ran (,)) β ((π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄)) β βπ β ran π
(π β π β§ π β π΄))) |
83 | 82 | rexlimivv 3198 |
. 2
β’
(βπ β ran
(,)βπ β ran
(,)(π΄ = (π Γ π) β§ (π β (β Γ β) β§
π β π΄)) β βπ β ran π
(π β π β§ π β π΄)) |
84 | 12, 14, 83 | 3syl 18 |
1
β’ ((π β (β Γ
β) β§ π΄ β
π΅ β§ π β π΄) β βπ β ran π
(π β π β§ π β π΄)) |