Step | Hyp | Ref
| Expression |
1 | | txcnp.4 |
. . . . . 6
β’ (π β π½ β (TopOnβπ)) |
2 | | txcnp.5 |
. . . . . 6
β’ (π β πΎ β (TopOnβπ)) |
3 | | txcnp.8 |
. . . . . 6
β’ (π β (π₯ β π β¦ π΄) β ((π½ CnP πΎ)βπ·)) |
4 | | cnpf2 13746 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ (π₯ β π β¦ π΄) β ((π½ CnP πΎ)βπ·)) β (π₯ β π β¦ π΄):πβΆπ) |
5 | 1, 2, 3, 4 | syl3anc 1238 |
. . . . 5
β’ (π β (π₯ β π β¦ π΄):πβΆπ) |
6 | 5 | fvmptelcdm 5671 |
. . . 4
β’ ((π β§ π₯ β π) β π΄ β π) |
7 | | txcnp.6 |
. . . . . 6
β’ (π β πΏ β (TopOnβπ)) |
8 | | txcnp.9 |
. . . . . 6
β’ (π β (π₯ β π β¦ π΅) β ((π½ CnP πΏ)βπ·)) |
9 | | cnpf2 13746 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΏ β (TopOnβπ) β§ (π₯ β π β¦ π΅) β ((π½ CnP πΏ)βπ·)) β (π₯ β π β¦ π΅):πβΆπ) |
10 | 1, 7, 8, 9 | syl3anc 1238 |
. . . . 5
β’ (π β (π₯ β π β¦ π΅):πβΆπ) |
11 | 10 | fvmptelcdm 5671 |
. . . 4
β’ ((π β§ π₯ β π) β π΅ β π) |
12 | 6, 11 | opelxpd 4661 |
. . 3
β’ ((π β§ π₯ β π) β β¨π΄, π΅β© β (π Γ π)) |
13 | 12 | fmpttd 5673 |
. 2
β’ (π β (π₯ β π β¦ β¨π΄, π΅β©):πβΆ(π Γ π)) |
14 | | txcnp.7 |
. . . . . . . . 9
β’ (π β π· β π) |
15 | | simpr 110 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β π₯ β π) |
16 | 12 | elexd 2752 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β β¨π΄, π΅β© β V) |
17 | | eqid 2177 |
. . . . . . . . . . . . 13
β’ (π₯ β π β¦ β¨π΄, π΅β©) = (π₯ β π β¦ β¨π΄, π΅β©) |
18 | 17 | fvmpt2 5601 |
. . . . . . . . . . . 12
β’ ((π₯ β π β§ β¨π΄, π΅β© β V) β ((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = β¨π΄, π΅β©) |
19 | 15, 16, 18 | syl2anc 411 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = β¨π΄, π΅β©) |
20 | | eqid 2177 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄) |
21 | 20 | fvmpt2 5601 |
. . . . . . . . . . . . 13
β’ ((π₯ β π β§ π΄ β π) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
22 | 15, 6, 21 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
23 | | eqid 2177 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β¦ π΅) = (π₯ β π β¦ π΅) |
24 | 23 | fvmpt2 5601 |
. . . . . . . . . . . . 13
β’ ((π₯ β π β§ π΅ β π) β ((π₯ β π β¦ π΅)βπ₯) = π΅) |
25 | 15, 11, 24 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ π΅)βπ₯) = π΅) |
26 | 22, 25 | opeq12d 3788 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© = β¨π΄, π΅β©) |
27 | 19, 26 | eqtr4d 2213 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) |
28 | 27 | ralrimiva 2550 |
. . . . . . . . 9
β’ (π β βπ₯ β π ((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) |
29 | | nffvmpt1 5528 |
. . . . . . . . . . 11
β’
β²π₯((π₯ β π β¦ β¨π΄, π΅β©)βπ·) |
30 | | nffvmpt1 5528 |
. . . . . . . . . . . 12
β’
β²π₯((π₯ β π β¦ π΄)βπ·) |
31 | | nffvmpt1 5528 |
. . . . . . . . . . . 12
β’
β²π₯((π₯ β π β¦ π΅)βπ·) |
32 | 30, 31 | nfop 3796 |
. . . . . . . . . . 11
β’
β²π₯β¨((π₯ β π β¦ π΄)βπ·), ((π₯ β π β¦ π΅)βπ·)β© |
33 | 29, 32 | nfeq 2327 |
. . . . . . . . . 10
β’
β²π₯((π₯ β π β¦ β¨π΄, π΅β©)βπ·) = β¨((π₯ β π β¦ π΄)βπ·), ((π₯ β π β¦ π΅)βπ·)β© |
34 | | fveq2 5517 |
. . . . . . . . . . 11
β’ (π₯ = π· β ((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = ((π₯ β π β¦ β¨π΄, π΅β©)βπ·)) |
35 | | fveq2 5517 |
. . . . . . . . . . . 12
β’ (π₯ = π· β ((π₯ β π β¦ π΄)βπ₯) = ((π₯ β π β¦ π΄)βπ·)) |
36 | | fveq2 5517 |
. . . . . . . . . . . 12
β’ (π₯ = π· β ((π₯ β π β¦ π΅)βπ₯) = ((π₯ β π β¦ π΅)βπ·)) |
37 | 35, 36 | opeq12d 3788 |
. . . . . . . . . . 11
β’ (π₯ = π· β β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© = β¨((π₯ β π β¦ π΄)βπ·), ((π₯ β π β¦ π΅)βπ·)β©) |
38 | 34, 37 | eqeq12d 2192 |
. . . . . . . . . 10
β’ (π₯ = π· β (((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© β ((π₯ β π β¦ β¨π΄, π΅β©)βπ·) = β¨((π₯ β π β¦ π΄)βπ·), ((π₯ β π β¦ π΅)βπ·)β©)) |
39 | 33, 38 | rspc 2837 |
. . . . . . . . 9
β’ (π· β π β (βπ₯ β π ((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© β ((π₯ β π β¦ β¨π΄, π΅β©)βπ·) = β¨((π₯ β π β¦ π΄)βπ·), ((π₯ β π β¦ π΅)βπ·)β©)) |
40 | 14, 28, 39 | sylc 62 |
. . . . . . . 8
β’ (π β ((π₯ β π β¦ β¨π΄, π΅β©)βπ·) = β¨((π₯ β π β¦ π΄)βπ·), ((π₯ β π β¦ π΅)βπ·)β©) |
41 | 40 | eleq1d 2246 |
. . . . . . 7
β’ (π β (((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β (π£ Γ π€) β β¨((π₯ β π β¦ π΄)βπ·), ((π₯ β π β¦ π΅)βπ·)β© β (π£ Γ π€))) |
42 | 41 | adantr 276 |
. . . . . 6
β’ ((π β§ (π£ β πΎ β§ π€ β πΏ)) β (((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β (π£ Γ π€) β β¨((π₯ β π β¦ π΄)βπ·), ((π₯ β π β¦ π΅)βπ·)β© β (π£ Γ π€))) |
43 | 1 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β π½ β (TopOnβπ)) |
44 | 2 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β πΎ β (TopOnβπ)) |
45 | 14 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β π· β π) |
46 | 3 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β (π₯ β π β¦ π΄) β ((π½ CnP πΎ)βπ·)) |
47 | | simplrl 535 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β π£ β πΎ) |
48 | | simprl 529 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β ((π₯ β π β¦ π΄)βπ·) β π£) |
49 | | icnpimaex 13750 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π· β π) β§ ((π₯ β π β¦ π΄) β ((π½ CnP πΎ)βπ·) β§ π£ β πΎ β§ ((π₯ β π β¦ π΄)βπ·) β π£)) β βπ β π½ (π· β π β§ ((π₯ β π β¦ π΄) β π) β π£)) |
50 | 43, 44, 45, 46, 47, 48, 49 | syl33anc 1253 |
. . . . . . . . 9
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β βπ β π½ (π· β π β§ ((π₯ β π β¦ π΄) β π) β π£)) |
51 | 7 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β πΏ β (TopOnβπ)) |
52 | 8 | ad2antrr 488 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β (π₯ β π β¦ π΅) β ((π½ CnP πΏ)βπ·)) |
53 | | simplrr 536 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β π€ β πΏ) |
54 | | simprr 531 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β ((π₯ β π β¦ π΅)βπ·) β π€) |
55 | | icnpimaex 13750 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΏ β (TopOnβπ) β§ π· β π) β§ ((π₯ β π β¦ π΅) β ((π½ CnP πΏ)βπ·) β§ π€ β πΏ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β βπ β π½ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)) |
56 | 43, 51, 45, 52, 53, 54, 55 | syl33anc 1253 |
. . . . . . . . 9
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β βπ β π½ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)) |
57 | 50, 56 | jca 306 |
. . . . . . . 8
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) β (βπ β π½ (π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ βπ β π½ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€))) |
58 | 57 | ex 115 |
. . . . . . 7
β’ ((π β§ (π£ β πΎ β§ π€ β πΏ)) β ((((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€) β (βπ β π½ (π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ βπ β π½ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)))) |
59 | | opelxp 4658 |
. . . . . . 7
β’
(β¨((π₯ β
π β¦ π΄)βπ·), ((π₯ β π β¦ π΅)βπ·)β© β (π£ Γ π€) β (((π₯ β π β¦ π΄)βπ·) β π£ β§ ((π₯ β π β¦ π΅)βπ·) β π€)) |
60 | | reeanv 2647 |
. . . . . . 7
β’
(βπ β
π½ βπ β π½ ((π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)) β (βπ β π½ (π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ βπ β π½ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€))) |
61 | 58, 59, 60 | 3imtr4g 205 |
. . . . . 6
β’ ((π β§ (π£ β πΎ β§ π€ β πΏ)) β (β¨((π₯ β π β¦ π΄)βπ·), ((π₯ β π β¦ π΅)βπ·)β© β (π£ Γ π€) β βπ β π½ βπ β π½ ((π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)))) |
62 | 42, 61 | sylbid 150 |
. . . . 5
β’ ((π β§ (π£ β πΎ β§ π€ β πΏ)) β (((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β (π£ Γ π€) β βπ β π½ βπ β π½ ((π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)))) |
63 | | an4 586 |
. . . . . . . . . . 11
β’ (((π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)) β ((π· β π β§ π· β π ) β§ (((π₯ β π β¦ π΄) β π) β π£ β§ ((π₯ β π β¦ π΅) β π ) β π€))) |
64 | | elin 3320 |
. . . . . . . . . . . . . 14
β’ (π· β (π β© π ) β (π· β π β§ π· β π )) |
65 | 64 | biimpri 133 |
. . . . . . . . . . . . 13
β’ ((π· β π β§ π· β π ) β π· β (π β© π )) |
66 | 65 | a1i 9 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (π β π½ β§ π β π½)) β ((π· β π β§ π· β π ) β π· β (π β© π ))) |
67 | | simpl 109 |
. . . . . . . . . . . . . . . 16
β’ ((π β π½ β§ π β π½) β π β π½) |
68 | | toponss 13565 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β (TopOnβπ) β§ π β π½) β π β π) |
69 | 1, 67, 68 | syl2an 289 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π½ β§ π β π½)) β π β π) |
70 | | ssinss1 3366 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β (π β© π ) β π) |
71 | 70 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β (π β© π ) β π) |
72 | 71 | sselda 3157 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β π‘ β π) |
73 | 28 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β βπ₯ β π ((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) |
74 | | nffvmpt1 5528 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯((π₯ β π β¦ β¨π΄, π΅β©)βπ‘) |
75 | | nffvmpt1 5528 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π₯((π₯ β π β¦ π΄)βπ‘) |
76 | | nffvmpt1 5528 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π₯((π₯ β π β¦ π΅)βπ‘) |
77 | 75, 76 | nfop 3796 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯β¨((π₯ β π β¦ π΄)βπ‘), ((π₯ β π β¦ π΅)βπ‘)β© |
78 | 74, 77 | nfeq 2327 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯((π₯ β π β¦ β¨π΄, π΅β©)βπ‘) = β¨((π₯ β π β¦ π΄)βπ‘), ((π₯ β π β¦ π΅)βπ‘)β© |
79 | | fveq2 5517 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π‘ β ((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = ((π₯ β π β¦ β¨π΄, π΅β©)βπ‘)) |
80 | | fveq2 5517 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π‘ β ((π₯ β π β¦ π΄)βπ₯) = ((π₯ β π β¦ π΄)βπ‘)) |
81 | | fveq2 5517 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π‘ β ((π₯ β π β¦ π΅)βπ₯) = ((π₯ β π β¦ π΅)βπ‘)) |
82 | 80, 81 | opeq12d 3788 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π‘ β β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© = β¨((π₯ β π β¦ π΄)βπ‘), ((π₯ β π β¦ π΅)βπ‘)β©) |
83 | 79, 82 | eqeq12d 2192 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π‘ β (((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© β ((π₯ β π β¦ β¨π΄, π΅β©)βπ‘) = β¨((π₯ β π β¦ π΄)βπ‘), ((π₯ β π β¦ π΅)βπ‘)β©)) |
84 | 78, 83 | rspc 2837 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ β π β (βπ₯ β π ((π₯ β π β¦ β¨π΄, π΅β©)βπ₯) = β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© β ((π₯ β π β¦ β¨π΄, π΅β©)βπ‘) = β¨((π₯ β π β¦ π΄)βπ‘), ((π₯ β π β¦ π΅)βπ‘)β©)) |
85 | 72, 73, 84 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β ((π₯ β π β¦ β¨π΄, π΅β©)βπ‘) = β¨((π₯ β π β¦ π΄)βπ‘), ((π₯ β π β¦ π΅)βπ‘)β©) |
86 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β π‘ β (π β© π )) |
87 | 86 | elin1d 3326 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β π‘ β π) |
88 | 5 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β (π₯ β π β¦ π΄):πβΆπ) |
89 | 88 | ffund 5371 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β Fun (π₯ β π β¦ π΄)) |
90 | 71 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β (π β© π ) β π) |
91 | 88 | fdmd 5374 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β dom (π₯ β π β¦ π΄) = π) |
92 | 90, 91 | sseqtrrd 3196 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β (π β© π ) β dom (π₯ β π β¦ π΄)) |
93 | 92, 86 | sseldd 3158 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β π‘ β dom (π₯ β π β¦ π΄)) |
94 | | funfvima 5750 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((Fun
(π₯ β π β¦ π΄) β§ π‘ β dom (π₯ β π β¦ π΄)) β (π‘ β π β ((π₯ β π β¦ π΄)βπ‘) β ((π₯ β π β¦ π΄) β π))) |
95 | 89, 93, 94 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β (π‘ β π β ((π₯ β π β¦ π΄)βπ‘) β ((π₯ β π β¦ π΄) β π))) |
96 | 87, 95 | mpd 13 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β ((π₯ β π β¦ π΄)βπ‘) β ((π₯ β π β¦ π΄) β π)) |
97 | 86 | elin2d 3327 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β π‘ β π ) |
98 | 10 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β (π₯ β π β¦ π΅):πβΆπ) |
99 | 98 | ffund 5371 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β Fun (π₯ β π β¦ π΅)) |
100 | 98 | fdmd 5374 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β dom (π₯ β π β¦ π΅) = π) |
101 | 90, 100 | sseqtrrd 3196 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β (π β© π ) β dom (π₯ β π β¦ π΅)) |
102 | 101, 86 | sseldd 3158 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β π‘ β dom (π₯ β π β¦ π΅)) |
103 | | funfvima 5750 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((Fun
(π₯ β π β¦ π΅) β§ π‘ β dom (π₯ β π β¦ π΅)) β (π‘ β π β ((π₯ β π β¦ π΅)βπ‘) β ((π₯ β π β¦ π΅) β π ))) |
104 | 99, 102, 103 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β (π‘ β π β ((π₯ β π β¦ π΅)βπ‘) β ((π₯ β π β¦ π΅) β π ))) |
105 | 97, 104 | mpd 13 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β ((π₯ β π β¦ π΅)βπ‘) β ((π₯ β π β¦ π΅) β π )) |
106 | 96, 105 | opelxpd 4661 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β β¨((π₯ β π β¦ π΄)βπ‘), ((π₯ β π β¦ π΅)βπ‘)β© β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π ))) |
107 | 85, 106 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π‘ β (π β© π )) β ((π₯ β π β¦ β¨π΄, π΅β©)βπ‘) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π ))) |
108 | 107 | ralrimiva 2550 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β βπ‘ β (π β© π )((π₯ β π β¦ β¨π΄, π΅β©)βπ‘) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π ))) |
109 | 13 | ffund 5371 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Fun (π₯ β π β¦ β¨π΄, π΅β©)) |
110 | 109 | adantr 276 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β Fun (π₯ β π β¦ β¨π΄, π΅β©)) |
111 | 13 | fdmd 5374 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β dom (π₯ β π β¦ β¨π΄, π΅β©) = π) |
112 | 111 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β dom (π₯ β π β¦ β¨π΄, π΅β©) = π) |
113 | 71, 112 | sseqtrrd 3196 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (π β© π ) β dom (π₯ β π β¦ β¨π΄, π΅β©)) |
114 | | funimass4 5568 |
. . . . . . . . . . . . . . . . 17
β’ ((Fun
(π₯ β π β¦ β¨π΄, π΅β©) β§ (π β© π ) β dom (π₯ β π β¦ β¨π΄, π΅β©)) β (((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π )) β βπ‘ β (π β© π )((π₯ β π β¦ β¨π΄, π΅β©)βπ‘) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π )))) |
115 | 110, 113,
114 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β (((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π )) β βπ‘ β (π β© π )((π₯ β π β¦ β¨π΄, π΅β©)βπ‘) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π )))) |
116 | 108, 115 | mpbird 167 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π ))) |
117 | 69, 116 | syldan 282 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π½ β§ π β π½)) β ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π ))) |
118 | 117 | adantlr 477 |
. . . . . . . . . . . . 13
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (π β π½ β§ π β π½)) β ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π ))) |
119 | | xpss12 4735 |
. . . . . . . . . . . . 13
β’ ((((π₯ β π β¦ π΄) β π) β π£ β§ ((π₯ β π β¦ π΅) β π ) β π€) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π )) β (π£ Γ π€)) |
120 | | sstr2 3164 |
. . . . . . . . . . . . 13
β’ (((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π )) β ((((π₯ β π β¦ π΄) β π) Γ ((π₯ β π β¦ π΅) β π )) β (π£ Γ π€) β ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (π£ Γ π€))) |
121 | 118, 119,
120 | syl2im 38 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (π β π½ β§ π β π½)) β ((((π₯ β π β¦ π΄) β π) β π£ β§ ((π₯ β π β¦ π΅) β π ) β π€) β ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (π£ Γ π€))) |
122 | 66, 121 | anim12d 335 |
. . . . . . . . . . 11
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (π β π½ β§ π β π½)) β (((π· β π β§ π· β π ) β§ (((π₯ β π β¦ π΄) β π) β π£ β§ ((π₯ β π β¦ π΅) β π ) β π€)) β (π· β (π β© π ) β§ ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (π£ Γ π€)))) |
123 | 63, 122 | biimtrid 152 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (π β π½ β§ π β π½)) β (((π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)) β (π· β (π β© π ) β§ ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (π£ Γ π€)))) |
124 | | topontop 13553 |
. . . . . . . . . . . . 13
β’ (π½ β (TopOnβπ) β π½ β Top) |
125 | 1, 124 | syl 14 |
. . . . . . . . . . . 12
β’ (π β π½ β Top) |
126 | | inopn 13542 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ π β π½ β§ π β π½) β (π β© π ) β π½) |
127 | 126 | 3expb 1204 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ (π β π½ β§ π β π½)) β (π β© π ) β π½) |
128 | 125, 127 | sylan 283 |
. . . . . . . . . . 11
β’ ((π β§ (π β π½ β§ π β π½)) β (π β© π ) β π½) |
129 | 128 | adantlr 477 |
. . . . . . . . . 10
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (π β π½ β§ π β π½)) β (π β© π ) β π½) |
130 | 123, 129 | jctild 316 |
. . . . . . . . 9
β’ (((π β§ (π£ β πΎ β§ π€ β πΏ)) β§ (π β π½ β§ π β π½)) β (((π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)) β ((π β© π ) β π½ β§ (π· β (π β© π ) β§ ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (π£ Γ π€))))) |
131 | 130 | expimpd 363 |
. . . . . . . 8
β’ ((π β§ (π£ β πΎ β§ π€ β πΏ)) β (((π β π½ β§ π β π½) β§ ((π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€))) β ((π β© π ) β π½ β§ (π· β (π β© π ) β§ ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (π£ Γ π€))))) |
132 | | eleq2 2241 |
. . . . . . . . . 10
β’ (π§ = (π β© π ) β (π· β π§ β π· β (π β© π ))) |
133 | | imaeq2 4968 |
. . . . . . . . . . 11
β’ (π§ = (π β© π ) β ((π₯ β π β¦ β¨π΄, π΅β©) β π§) = ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π ))) |
134 | 133 | sseq1d 3186 |
. . . . . . . . . 10
β’ (π§ = (π β© π ) β (((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€) β ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (π£ Γ π€))) |
135 | 132, 134 | anbi12d 473 |
. . . . . . . . 9
β’ (π§ = (π β© π ) β ((π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€)) β (π· β (π β© π ) β§ ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (π£ Γ π€)))) |
136 | 135 | rspcev 2843 |
. . . . . . . 8
β’ (((π β© π ) β π½ β§ (π· β (π β© π ) β§ ((π₯ β π β¦ β¨π΄, π΅β©) β (π β© π )) β (π£ Γ π€))) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€))) |
137 | 131, 136 | syl6 33 |
. . . . . . 7
β’ ((π β§ (π£ β πΎ β§ π€ β πΏ)) β (((π β π½ β§ π β π½) β§ ((π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€))) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€)))) |
138 | 137 | expd 258 |
. . . . . 6
β’ ((π β§ (π£ β πΎ β§ π€ β πΏ)) β ((π β π½ β§ π β π½) β (((π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€))))) |
139 | 138 | rexlimdvv 2601 |
. . . . 5
β’ ((π β§ (π£ β πΎ β§ π€ β πΏ)) β (βπ β π½ βπ β π½ ((π· β π β§ ((π₯ β π β¦ π΄) β π) β π£) β§ (π· β π β§ ((π₯ β π β¦ π΅) β π ) β π€)) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€)))) |
140 | 62, 139 | syld 45 |
. . . 4
β’ ((π β§ (π£ β πΎ β§ π€ β πΏ)) β (((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β (π£ Γ π€) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€)))) |
141 | 140 | ralrimivva 2559 |
. . 3
β’ (π β βπ£ β πΎ βπ€ β πΏ (((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β (π£ Γ π€) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€)))) |
142 | | vex 2742 |
. . . . . 6
β’ π£ β V |
143 | | vex 2742 |
. . . . . 6
β’ π€ β V |
144 | 142, 143 | xpex 4743 |
. . . . 5
β’ (π£ Γ π€) β V |
145 | 144 | rgen2w 2533 |
. . . 4
β’
βπ£ β
πΎ βπ€ β πΏ (π£ Γ π€) β V |
146 | | eqid 2177 |
. . . . 5
β’ (π£ β πΎ, π€ β πΏ β¦ (π£ Γ π€)) = (π£ β πΎ, π€ β πΏ β¦ (π£ Γ π€)) |
147 | | eleq2 2241 |
. . . . . 6
β’ (π¦ = (π£ Γ π€) β (((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β π¦ β ((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β (π£ Γ π€))) |
148 | | sseq2 3181 |
. . . . . . . 8
β’ (π¦ = (π£ Γ π€) β (((π₯ β π β¦ β¨π΄, π΅β©) β π§) β π¦ β ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€))) |
149 | 148 | anbi2d 464 |
. . . . . . 7
β’ (π¦ = (π£ Γ π€) β ((π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β π¦) β (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€)))) |
150 | 149 | rexbidv 2478 |
. . . . . 6
β’ (π¦ = (π£ Γ π€) β (βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β π¦) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€)))) |
151 | 147, 150 | imbi12d 234 |
. . . . 5
β’ (π¦ = (π£ Γ π€) β ((((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β π¦ β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β π¦)) β (((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β (π£ Γ π€) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€))))) |
152 | 146, 151 | ralrnmpo 5991 |
. . . 4
β’
(βπ£ β
πΎ βπ€ β πΏ (π£ Γ π€) β V β (βπ¦ β ran (π£ β πΎ, π€ β πΏ β¦ (π£ Γ π€))(((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β π¦ β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β π¦)) β βπ£ β πΎ βπ€ β πΏ (((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β (π£ Γ π€) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€))))) |
153 | 145, 152 | ax-mp 5 |
. . 3
β’
(βπ¦ β
ran (π£ β πΎ, π€ β πΏ β¦ (π£ Γ π€))(((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β π¦ β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β π¦)) β βπ£ β πΎ βπ€ β πΏ (((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β (π£ Γ π€) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β (π£ Γ π€)))) |
154 | 141, 153 | sylibr 134 |
. 2
β’ (π β βπ¦ β ran (π£ β πΎ, π€ β πΏ β¦ (π£ Γ π€))(((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β π¦ β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β π¦))) |
155 | | topontop 13553 |
. . . . 5
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
156 | 2, 155 | syl 14 |
. . . 4
β’ (π β πΎ β Top) |
157 | | topontop 13553 |
. . . . 5
β’ (πΏ β (TopOnβπ) β πΏ β Top) |
158 | 7, 157 | syl 14 |
. . . 4
β’ (π β πΏ β Top) |
159 | | eqid 2177 |
. . . . 5
β’ ran
(π£ β πΎ, π€ β πΏ β¦ (π£ Γ π€)) = ran (π£ β πΎ, π€ β πΏ β¦ (π£ Γ π€)) |
160 | 159 | txval 13794 |
. . . 4
β’ ((πΎ β Top β§ πΏ β Top) β (πΎ Γt πΏ) = (topGenβran (π£ β πΎ, π€ β πΏ β¦ (π£ Γ π€)))) |
161 | 156, 158,
160 | syl2anc 411 |
. . 3
β’ (π β (πΎ Γt πΏ) = (topGenβran (π£ β πΎ, π€ β πΏ β¦ (π£ Γ π€)))) |
162 | | txtopon 13801 |
. . . 4
β’ ((πΎ β (TopOnβπ) β§ πΏ β (TopOnβπ)) β (πΎ Γt πΏ) β (TopOnβ(π Γ π))) |
163 | 2, 7, 162 | syl2anc 411 |
. . 3
β’ (π β (πΎ Γt πΏ) β (TopOnβ(π Γ π))) |
164 | 1, 161, 163, 14 | tgcnp 13748 |
. 2
β’ (π β ((π₯ β π β¦ β¨π΄, π΅β©) β ((π½ CnP (πΎ Γt πΏ))βπ·) β ((π₯ β π β¦ β¨π΄, π΅β©):πβΆ(π Γ π) β§ βπ¦ β ran (π£ β πΎ, π€ β πΏ β¦ (π£ Γ π€))(((π₯ β π β¦ β¨π΄, π΅β©)βπ·) β π¦ β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ β¨π΄, π΅β©) β π§) β π¦))))) |
165 | 13, 154, 164 | mpbir2and 944 |
1
β’ (π β (π₯ β π β¦ β¨π΄, π΅β©) β ((π½ CnP (πΎ Γt πΏ))βπ·)) |