Step | Hyp | Ref
| Expression |
1 | | txdis1cn.f |
. . 3
β’ (π β πΉ Fn (π Γ π)) |
2 | | txdis1cn.j |
. . . . . . 7
β’ (π β π½ β (TopOnβπ)) |
3 | 2 | adantr 276 |
. . . . . 6
β’ ((π β§ π₯ β π) β π½ β (TopOnβπ)) |
4 | | txdis1cn.k |
. . . . . . . 8
β’ (π β πΎ β Top) |
5 | | toptopon2 13558 |
. . . . . . . 8
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
6 | 4, 5 | sylib 122 |
. . . . . . 7
β’ (π β πΎ β (TopOnββͺ πΎ)) |
7 | 6 | adantr 276 |
. . . . . 6
β’ ((π β§ π₯ β π) β πΎ β (TopOnββͺ πΎ)) |
8 | | txdis1cn.1 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π¦ β π β¦ (π₯πΉπ¦)) β (π½ Cn πΎ)) |
9 | | cnf2 13744 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ)
β§ (π¦ β π β¦ (π₯πΉπ¦)) β (π½ Cn πΎ)) β (π¦ β π β¦ (π₯πΉπ¦)):πβΆβͺ πΎ) |
10 | 3, 7, 8, 9 | syl3anc 1238 |
. . . . 5
β’ ((π β§ π₯ β π) β (π¦ β π β¦ (π₯πΉπ¦)):πβΆβͺ πΎ) |
11 | | eqid 2177 |
. . . . . 6
β’ (π¦ β π β¦ (π₯πΉπ¦)) = (π¦ β π β¦ (π₯πΉπ¦)) |
12 | 11 | fmpt 5668 |
. . . . 5
β’
(βπ¦ β
π (π₯πΉπ¦) β βͺ πΎ β (π¦ β π β¦ (π₯πΉπ¦)):πβΆβͺ πΎ) |
13 | 10, 12 | sylibr 134 |
. . . 4
β’ ((π β§ π₯ β π) β βπ¦ β π (π₯πΉπ¦) β βͺ πΎ) |
14 | 13 | ralrimiva 2550 |
. . 3
β’ (π β βπ₯ β π βπ¦ β π (π₯πΉπ¦) β βͺ πΎ) |
15 | | ffnov 5981 |
. . 3
β’ (πΉ:(π Γ π)βΆβͺ πΎ β (πΉ Fn (π Γ π) β§ βπ₯ β π βπ¦ β π (π₯πΉπ¦) β βͺ πΎ)) |
16 | 1, 14, 15 | sylanbrc 417 |
. 2
β’ (π β πΉ:(π Γ π)βΆβͺ πΎ) |
17 | | cnvimass 4993 |
. . . . . . . 8
β’ (β‘πΉ β π’) β dom πΉ |
18 | 1 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π’ β πΎ) β πΉ Fn (π Γ π)) |
19 | | fndm 5317 |
. . . . . . . . 9
β’ (πΉ Fn (π Γ π) β dom πΉ = (π Γ π)) |
20 | 18, 19 | syl 14 |
. . . . . . . 8
β’ ((π β§ π’ β πΎ) β dom πΉ = (π Γ π)) |
21 | 17, 20 | sseqtrid 3207 |
. . . . . . 7
β’ ((π β§ π’ β πΎ) β (β‘πΉ β π’) β (π Γ π)) |
22 | | relxp 4737 |
. . . . . . 7
β’ Rel
(π Γ π) |
23 | | relss 4715 |
. . . . . . 7
β’ ((β‘πΉ β π’) β (π Γ π) β (Rel (π Γ π) β Rel (β‘πΉ β π’))) |
24 | 21, 22, 23 | mpisyl 1446 |
. . . . . 6
β’ ((π β§ π’ β πΎ) β Rel (β‘πΉ β π’)) |
25 | | elpreima 5637 |
. . . . . . . 8
β’ (πΉ Fn (π Γ π) β (β¨π₯, π§β© β (β‘πΉ β π’) β (β¨π₯, π§β© β (π Γ π) β§ (πΉββ¨π₯, π§β©) β π’))) |
26 | 18, 25 | syl 14 |
. . . . . . 7
β’ ((π β§ π’ β πΎ) β (β¨π₯, π§β© β (β‘πΉ β π’) β (β¨π₯, π§β© β (π Γ π) β§ (πΉββ¨π₯, π§β©) β π’))) |
27 | | opelxp 4658 |
. . . . . . . . 9
β’
(β¨π₯, π§β© β (π Γ π) β (π₯ β π β§ π§ β π)) |
28 | | df-ov 5880 |
. . . . . . . . . . 11
β’ (π₯πΉπ§) = (πΉββ¨π₯, π§β©) |
29 | 28 | eqcomi 2181 |
. . . . . . . . . 10
β’ (πΉββ¨π₯, π§β©) = (π₯πΉπ§) |
30 | 29 | eleq1i 2243 |
. . . . . . . . 9
β’ ((πΉββ¨π₯, π§β©) β π’ β (π₯πΉπ§) β π’) |
31 | 27, 30 | anbi12i 460 |
. . . . . . . 8
β’
((β¨π₯, π§β© β (π Γ π) β§ (πΉββ¨π₯, π§β©) β π’) β ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) |
32 | | simprll 537 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β π₯ β π) |
33 | | snelpwi 4214 |
. . . . . . . . . . . 12
β’ (π₯ β π β {π₯} β π« π) |
34 | 32, 33 | syl 14 |
. . . . . . . . . . 11
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β {π₯} β π« π) |
35 | 11 | mptpreima 5124 |
. . . . . . . . . . . 12
β’ (β‘(π¦ β π β¦ (π₯πΉπ¦)) β π’) = {π¦ β π β£ (π₯πΉπ¦) β π’} |
36 | 8 | adantrr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π β§ π§ β π)) β (π¦ β π β¦ (π₯πΉπ¦)) β (π½ Cn πΎ)) |
37 | 36 | ad2ant2r 509 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β (π¦ β π β¦ (π₯πΉπ¦)) β (π½ Cn πΎ)) |
38 | | simplr 528 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β π’ β πΎ) |
39 | | cnima 13759 |
. . . . . . . . . . . . 13
β’ (((π¦ β π β¦ (π₯πΉπ¦)) β (π½ Cn πΎ) β§ π’ β πΎ) β (β‘(π¦ β π β¦ (π₯πΉπ¦)) β π’) β π½) |
40 | 37, 38, 39 | syl2anc 411 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β (β‘(π¦ β π β¦ (π₯πΉπ¦)) β π’) β π½) |
41 | 35, 40 | eqeltrrid 2265 |
. . . . . . . . . . 11
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β {π¦ β π β£ (π₯πΉπ¦) β π’} β π½) |
42 | | simprlr 538 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β π§ β π) |
43 | | simprr 531 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β (π₯πΉπ§) β π’) |
44 | | vsnid 3626 |
. . . . . . . . . . . . . 14
β’ π₯ β {π₯} |
45 | | opelxp 4658 |
. . . . . . . . . . . . . 14
β’
(β¨π₯, π§β© β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β (π₯ β {π₯} β§ π§ β {π¦ β π β£ (π₯πΉπ¦) β π’})) |
46 | 44, 45 | mpbiran 940 |
. . . . . . . . . . . . 13
β’
(β¨π₯, π§β© β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β π§ β {π¦ β π β£ (π₯πΉπ¦) β π’}) |
47 | | oveq2 5885 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π§ β (π₯πΉπ¦) = (π₯πΉπ§)) |
48 | 47 | eleq1d 2246 |
. . . . . . . . . . . . . 14
β’ (π¦ = π§ β ((π₯πΉπ¦) β π’ β (π₯πΉπ§) β π’)) |
49 | 48 | elrab 2895 |
. . . . . . . . . . . . 13
β’ (π§ β {π¦ β π β£ (π₯πΉπ¦) β π’} β (π§ β π β§ (π₯πΉπ§) β π’)) |
50 | 46, 49 | bitri 184 |
. . . . . . . . . . . 12
β’
(β¨π₯, π§β© β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β (π§ β π β§ (π₯πΉπ§) β π’)) |
51 | 42, 43, 50 | sylanbrc 417 |
. . . . . . . . . . 11
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β β¨π₯, π§β© β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’})) |
52 | | relxp 4737 |
. . . . . . . . . . . . 13
β’ Rel
({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) |
53 | 52 | a1i 9 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β Rel ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’})) |
54 | | opelxp 4658 |
. . . . . . . . . . . . 13
β’
(β¨π, πβ© β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) |
55 | 32 | snssd 3739 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β {π₯} β π) |
56 | 55 | sselda 3157 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ π β {π₯}) β π β π) |
57 | 56 | adantrr 479 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) β π β π) |
58 | | elrabi 2892 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π¦ β π β£ (π₯πΉπ¦) β π’} β π β π) |
59 | 58 | ad2antll 491 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) β π β π) |
60 | 57, 59 | opelxpd 4661 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) β β¨π, πβ© β (π Γ π)) |
61 | | df-ov 5880 |
. . . . . . . . . . . . . . . . 17
β’ (ππΉπ) = (πΉββ¨π, πβ©) |
62 | | elsni 3612 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π₯} β π = π₯) |
63 | 62 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) β π = π₯) |
64 | 63 | oveq1d 5892 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) β (ππΉπ) = (π₯πΉπ)) |
65 | 61, 64 | eqtr3id 2224 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) β (πΉββ¨π, πβ©) = (π₯πΉπ)) |
66 | | oveq2 5885 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β (π₯πΉπ¦) = (π₯πΉπ)) |
67 | 66 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β ((π₯πΉπ¦) β π’ β (π₯πΉπ) β π’)) |
68 | 67 | elrab 2895 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {π¦ β π β£ (π₯πΉπ¦) β π’} β (π β π β§ (π₯πΉπ) β π’)) |
69 | 68 | simprbi 275 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π¦ β π β£ (π₯πΉπ¦) β π’} β (π₯πΉπ) β π’) |
70 | 69 | ad2antll 491 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) β (π₯πΉπ) β π’) |
71 | 65, 70 | eqeltrd 2254 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) β (πΉββ¨π, πβ©) β π’) |
72 | | elpreima 5637 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ Fn (π Γ π) β (β¨π, πβ© β (β‘πΉ β π’) β (β¨π, πβ© β (π Γ π) β§ (πΉββ¨π, πβ©) β π’))) |
73 | 1, 72 | syl 14 |
. . . . . . . . . . . . . . . 16
β’ (π β (β¨π, πβ© β (β‘πΉ β π’) β (β¨π, πβ© β (π Γ π) β§ (πΉββ¨π, πβ©) β π’))) |
74 | 73 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) β (β¨π, πβ© β (β‘πΉ β π’) β (β¨π, πβ© β (π Γ π) β§ (πΉββ¨π, πβ©) β π’))) |
75 | 60, 71, 74 | mpbir2and 944 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β§ (π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’})) β β¨π, πβ© β (β‘πΉ β π’)) |
76 | 75 | ex 115 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β ((π β {π₯} β§ π β {π¦ β π β£ (π₯πΉπ¦) β π’}) β β¨π, πβ© β (β‘πΉ β π’))) |
77 | 54, 76 | biimtrid 152 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β (β¨π, πβ© β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β β¨π, πβ© β (β‘πΉ β π’))) |
78 | 53, 77 | relssdv 4720 |
. . . . . . . . . . 11
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β (β‘πΉ β π’)) |
79 | | xpeq1 4642 |
. . . . . . . . . . . . . 14
β’ (π = {π₯} β (π Γ π) = ({π₯} Γ π)) |
80 | 79 | eleq2d 2247 |
. . . . . . . . . . . . 13
β’ (π = {π₯} β (β¨π₯, π§β© β (π Γ π) β β¨π₯, π§β© β ({π₯} Γ π))) |
81 | 79 | sseq1d 3186 |
. . . . . . . . . . . . 13
β’ (π = {π₯} β ((π Γ π) β (β‘πΉ β π’) β ({π₯} Γ π) β (β‘πΉ β π’))) |
82 | 80, 81 | anbi12d 473 |
. . . . . . . . . . . 12
β’ (π = {π₯} β ((β¨π₯, π§β© β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’)) β (β¨π₯, π§β© β ({π₯} Γ π) β§ ({π₯} Γ π) β (β‘πΉ β π’)))) |
83 | | xpeq2 4643 |
. . . . . . . . . . . . . 14
β’ (π = {π¦ β π β£ (π₯πΉπ¦) β π’} β ({π₯} Γ π) = ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’})) |
84 | 83 | eleq2d 2247 |
. . . . . . . . . . . . 13
β’ (π = {π¦ β π β£ (π₯πΉπ¦) β π’} β (β¨π₯, π§β© β ({π₯} Γ π) β β¨π₯, π§β© β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}))) |
85 | 83 | sseq1d 3186 |
. . . . . . . . . . . . 13
β’ (π = {π¦ β π β£ (π₯πΉπ¦) β π’} β (({π₯} Γ π) β (β‘πΉ β π’) β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β (β‘πΉ β π’))) |
86 | 84, 85 | anbi12d 473 |
. . . . . . . . . . . 12
β’ (π = {π¦ β π β£ (π₯πΉπ¦) β π’} β ((β¨π₯, π§β© β ({π₯} Γ π) β§ ({π₯} Γ π) β (β‘πΉ β π’)) β (β¨π₯, π§β© β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β§ ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β (β‘πΉ β π’)))) |
87 | 82, 86 | rspc2ev 2858 |
. . . . . . . . . . 11
β’ (({π₯} β π« π β§ {π¦ β π β£ (π₯πΉπ¦) β π’} β π½ β§ (β¨π₯, π§β© β ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β§ ({π₯} Γ {π¦ β π β£ (π₯πΉπ¦) β π’}) β (β‘πΉ β π’))) β βπ β π« πβπ β π½ (β¨π₯, π§β© β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))) |
88 | 34, 41, 51, 78, 87 | syl112anc 1242 |
. . . . . . . . . 10
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β βπ β π« πβπ β π½ (β¨π₯, π§β© β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))) |
89 | | vex 2742 |
. . . . . . . . . . . 12
β’ π₯ β V |
90 | | vex 2742 |
. . . . . . . . . . . 12
β’ π§ β V |
91 | 89, 90 | opex 4231 |
. . . . . . . . . . 11
β’
β¨π₯, π§β© β V |
92 | | eleq1 2240 |
. . . . . . . . . . . . 13
β’ (π£ = β¨π₯, π§β© β (π£ β (π Γ π) β β¨π₯, π§β© β (π Γ π))) |
93 | 92 | anbi1d 465 |
. . . . . . . . . . . 12
β’ (π£ = β¨π₯, π§β© β ((π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’)) β (β¨π₯, π§β© β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’)))) |
94 | 93 | 2rexbidv 2502 |
. . . . . . . . . . 11
β’ (π£ = β¨π₯, π§β© β (βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’)) β βπ β π« πβπ β π½ (β¨π₯, π§β© β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’)))) |
95 | 91, 94 | elab 2883 |
. . . . . . . . . 10
β’
(β¨π₯, π§β© β {π£ β£ βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))} β βπ β π« πβπ β π½ (β¨π₯, π§β© β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))) |
96 | 88, 95 | sylibr 134 |
. . . . . . . . 9
β’ (((π β§ π’ β πΎ) β§ ((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’)) β β¨π₯, π§β© β {π£ β£ βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))}) |
97 | 96 | ex 115 |
. . . . . . . 8
β’ ((π β§ π’ β πΎ) β (((π₯ β π β§ π§ β π) β§ (π₯πΉπ§) β π’) β β¨π₯, π§β© β {π£ β£ βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))})) |
98 | 31, 97 | biimtrid 152 |
. . . . . . 7
β’ ((π β§ π’ β πΎ) β ((β¨π₯, π§β© β (π Γ π) β§ (πΉββ¨π₯, π§β©) β π’) β β¨π₯, π§β© β {π£ β£ βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))})) |
99 | 26, 98 | sylbid 150 |
. . . . . 6
β’ ((π β§ π’ β πΎ) β (β¨π₯, π§β© β (β‘πΉ β π’) β β¨π₯, π§β© β {π£ β£ βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))})) |
100 | 24, 99 | relssdv 4720 |
. . . . 5
β’ ((π β§ π’ β πΎ) β (β‘πΉ β π’) β {π£ β£ βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))}) |
101 | | ssabral 3228 |
. . . . 5
β’ ((β‘πΉ β π’) β {π£ β£ βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))} β βπ£ β (β‘πΉ β π’)βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))) |
102 | 100, 101 | sylib 122 |
. . . 4
β’ ((π β§ π’ β πΎ) β βπ£ β (β‘πΉ β π’)βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’))) |
103 | | txdis1cn.x |
. . . . . . 7
β’ (π β π β π) |
104 | | distopon 13626 |
. . . . . . 7
β’ (π β π β π« π β (TopOnβπ)) |
105 | 103, 104 | syl 14 |
. . . . . 6
β’ (π β π« π β (TopOnβπ)) |
106 | 105 | adantr 276 |
. . . . 5
β’ ((π β§ π’ β πΎ) β π« π β (TopOnβπ)) |
107 | 2 | adantr 276 |
. . . . 5
β’ ((π β§ π’ β πΎ) β π½ β (TopOnβπ)) |
108 | | eltx 13798 |
. . . . 5
β’
((π« π β
(TopOnβπ) β§ π½ β (TopOnβπ)) β ((β‘πΉ β π’) β (π« π Γt π½) β βπ£ β (β‘πΉ β π’)βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’)))) |
109 | 106, 107,
108 | syl2anc 411 |
. . . 4
β’ ((π β§ π’ β πΎ) β ((β‘πΉ β π’) β (π« π Γt π½) β βπ£ β (β‘πΉ β π’)βπ β π« πβπ β π½ (π£ β (π Γ π) β§ (π Γ π) β (β‘πΉ β π’)))) |
110 | 102, 109 | mpbird 167 |
. . 3
β’ ((π β§ π’ β πΎ) β (β‘πΉ β π’) β (π« π Γt π½)) |
111 | 110 | ralrimiva 2550 |
. 2
β’ (π β βπ’ β πΎ (β‘πΉ β π’) β (π« π Γt π½)) |
112 | | txtopon 13801 |
. . . 4
β’
((π« π β
(TopOnβπ) β§ π½ β (TopOnβπ)) β (π« π Γt π½) β (TopOnβ(π Γ π))) |
113 | 105, 2, 112 | syl2anc 411 |
. . 3
β’ (π β (π« π Γt π½) β (TopOnβ(π Γ π))) |
114 | | iscn 13736 |
. . 3
β’
(((π« π
Γt π½)
β (TopOnβ(π
Γ π)) β§ πΎ β (TopOnββͺ πΎ))
β (πΉ β
((π« π
Γt π½) Cn
πΎ) β (πΉ:(π Γ π)βΆβͺ πΎ β§ βπ’ β πΎ (β‘πΉ β π’) β (π« π Γt π½)))) |
115 | 113, 6, 114 | syl2anc 411 |
. 2
β’ (π β (πΉ β ((π« π Γt π½) Cn πΎ) β (πΉ:(π Γ π)βΆβͺ πΎ β§ βπ’ β πΎ (β‘πΉ β π’) β (π« π Γt π½)))) |
116 | 16, 111, 115 | mpbir2and 944 |
1
β’ (π β πΉ β ((π« π Γt π½) Cn πΎ)) |