Step | Hyp | Ref
| Expression |
1 | | txcnpi.3 |
. . 3
β’ (π β πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π΄, π΅β©)) |
2 | | txcnpi.4 |
. . 3
β’ (π β π β πΏ) |
3 | | df-ov 7306 |
. . . 4
β’ (π΄πΉπ΅) = (πΉββ¨π΄, π΅β©) |
4 | | txcnpi.7 |
. . . 4
β’ (π β (π΄πΉπ΅) β π) |
5 | 3, 4 | eqeltrrid 2842 |
. . 3
β’ (π β (πΉββ¨π΄, π΅β©) β π) |
6 | | cnpimaex 22448 |
. . 3
β’ ((πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π΄, π΅β©) β§ π β πΏ β§ (πΉββ¨π΄, π΅β©) β π) β βπ€ β (π½ Γt πΎ)(β¨π΄, π΅β© β π€ β§ (πΉ β π€) β π)) |
7 | 1, 2, 5, 6 | syl3anc 1371 |
. 2
β’ (π β βπ€ β (π½ Γt πΎ)(β¨π΄, π΅β© β π€ β§ (πΉ β π€) β π)) |
8 | | eqid 2736 |
. . . . . . . . . 10
β’ βͺ (π½
Γt πΎ) =
βͺ (π½ Γt πΎ) |
9 | | eqid 2736 |
. . . . . . . . . 10
β’ βͺ πΏ =
βͺ πΏ |
10 | 8, 9 | cnpf 22439 |
. . . . . . . . 9
β’ (πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π΄, π΅β©) β πΉ:βͺ (π½ Γt πΎ)βΆβͺ πΏ) |
11 | 1, 10 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:βͺ (π½ Γt πΎ)βΆβͺ πΏ) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π€ β (π½ Γt πΎ)) β πΉ:βͺ (π½ Γt πΎ)βΆβͺ πΏ) |
13 | 12 | ffund 6630 |
. . . . . 6
β’ ((π β§ π€ β (π½ Γt πΎ)) β Fun πΉ) |
14 | | elssuni 4877 |
. . . . . . 7
β’ (π€ β (π½ Γt πΎ) β π€ β βͺ (π½ Γt πΎ)) |
15 | 11 | fdmd 6637 |
. . . . . . . . 9
β’ (π β dom πΉ = βͺ (π½ Γt πΎ)) |
16 | 15 | sseq2d 3958 |
. . . . . . . 8
β’ (π β (π€ β dom πΉ β π€ β βͺ (π½ Γt πΎ))) |
17 | 16 | biimpar 479 |
. . . . . . 7
β’ ((π β§ π€ β βͺ (π½ Γt πΎ)) β π€ β dom πΉ) |
18 | 14, 17 | sylan2 594 |
. . . . . 6
β’ ((π β§ π€ β (π½ Γt πΎ)) β π€ β dom πΉ) |
19 | | funimass3 6959 |
. . . . . 6
β’ ((Fun
πΉ β§ π€ β dom πΉ) β ((πΉ β π€) β π β π€ β (β‘πΉ β π))) |
20 | 13, 18, 19 | syl2anc 585 |
. . . . 5
β’ ((π β§ π€ β (π½ Γt πΎ)) β ((πΉ β π€) β π β π€ β (β‘πΉ β π))) |
21 | 20 | anbi2d 630 |
. . . 4
β’ ((π β§ π€ β (π½ Γt πΎ)) β ((β¨π΄, π΅β© β π€ β§ (πΉ β π€) β π) β (β¨π΄, π΅β© β π€ β§ π€ β (β‘πΉ β π)))) |
22 | | txcnpi.1 |
. . . . . . 7
β’ (π β π½ β (TopOnβπ)) |
23 | | txcnpi.2 |
. . . . . . 7
β’ (π β πΎ β (TopOnβπ)) |
24 | | eltx 22760 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π€ β (π½ Γt πΎ) β βπ§ β π€ βπ’ β π½ βπ£ β πΎ (π§ β (π’ Γ π£) β§ (π’ Γ π£) β π€))) |
25 | 22, 23, 24 | syl2anc 585 |
. . . . . 6
β’ (π β (π€ β (π½ Γt πΎ) β βπ§ β π€ βπ’ β π½ βπ£ β πΎ (π§ β (π’ Γ π£) β§ (π’ Γ π£) β π€))) |
26 | 25 | biimpa 478 |
. . . . 5
β’ ((π β§ π€ β (π½ Γt πΎ)) β βπ§ β π€ βπ’ β π½ βπ£ β πΎ (π§ β (π’ Γ π£) β§ (π’ Γ π£) β π€)) |
27 | | eleq1 2824 |
. . . . . . . . . 10
β’ (π§ = β¨π΄, π΅β© β (π§ β (π’ Γ π£) β β¨π΄, π΅β© β (π’ Γ π£))) |
28 | 27 | anbi1d 631 |
. . . . . . . . 9
β’ (π§ = β¨π΄, π΅β© β ((π§ β (π’ Γ π£) β§ (π’ Γ π£) β π€) β (β¨π΄, π΅β© β (π’ Γ π£) β§ (π’ Γ π£) β π€))) |
29 | 28 | 2rexbidv 3210 |
. . . . . . . 8
β’ (π§ = β¨π΄, π΅β© β (βπ’ β π½ βπ£ β πΎ (π§ β (π’ Γ π£) β§ (π’ Γ π£) β π€) β βπ’ β π½ βπ£ β πΎ (β¨π΄, π΅β© β (π’ Γ π£) β§ (π’ Γ π£) β π€))) |
30 | 29 | rspccv 3563 |
. . . . . . 7
β’
(βπ§ β
π€ βπ’ β π½ βπ£ β πΎ (π§ β (π’ Γ π£) β§ (π’ Γ π£) β π€) β (β¨π΄, π΅β© β π€ β βπ’ β π½ βπ£ β πΎ (β¨π΄, π΅β© β (π’ Γ π£) β§ (π’ Γ π£) β π€))) |
31 | | sstr2 3933 |
. . . . . . . . . . . . 13
β’ ((π’ Γ π£) β π€ β (π€ β (β‘πΉ β π) β (π’ Γ π£) β (β‘πΉ β π))) |
32 | 31 | com12 32 |
. . . . . . . . . . . 12
β’ (π€ β (β‘πΉ β π) β ((π’ Γ π£) β π€ β (π’ Γ π£) β (β‘πΉ β π))) |
33 | 32 | anim2d 613 |
. . . . . . . . . . 11
β’ (π€ β (β‘πΉ β π) β (((π΄ β π’ β§ π΅ β π£) β§ (π’ Γ π£) β π€) β ((π΄ β π’ β§ π΅ β π£) β§ (π’ Γ π£) β (β‘πΉ β π)))) |
34 | | opelxp 5632 |
. . . . . . . . . . . 12
β’
(β¨π΄, π΅β© β (π’ Γ π£) β (π΄ β π’ β§ π΅ β π£)) |
35 | 34 | anbi1i 625 |
. . . . . . . . . . 11
β’
((β¨π΄, π΅β© β (π’ Γ π£) β§ (π’ Γ π£) β π€) β ((π΄ β π’ β§ π΅ β π£) β§ (π’ Γ π£) β π€)) |
36 | | df-3an 1089 |
. . . . . . . . . . 11
β’ ((π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π)) β ((π΄ β π’ β§ π΅ β π£) β§ (π’ Γ π£) β (β‘πΉ β π))) |
37 | 33, 35, 36 | 3imtr4g 297 |
. . . . . . . . . 10
β’ (π€ β (β‘πΉ β π) β ((β¨π΄, π΅β© β (π’ Γ π£) β§ (π’ Γ π£) β π€) β (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π)))) |
38 | 37 | reximdv 3164 |
. . . . . . . . 9
β’ (π€ β (β‘πΉ β π) β (βπ£ β πΎ (β¨π΄, π΅β© β (π’ Γ π£) β§ (π’ Γ π£) β π€) β βπ£ β πΎ (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π)))) |
39 | 38 | reximdv 3164 |
. . . . . . . 8
β’ (π€ β (β‘πΉ β π) β (βπ’ β π½ βπ£ β πΎ (β¨π΄, π΅β© β (π’ Γ π£) β§ (π’ Γ π£) β π€) β βπ’ β π½ βπ£ β πΎ (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π)))) |
40 | 39 | com12 32 |
. . . . . . 7
β’
(βπ’ β
π½ βπ£ β πΎ (β¨π΄, π΅β© β (π’ Γ π£) β§ (π’ Γ π£) β π€) β (π€ β (β‘πΉ β π) β βπ’ β π½ βπ£ β πΎ (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π)))) |
41 | 30, 40 | syl6 35 |
. . . . . 6
β’
(βπ§ β
π€ βπ’ β π½ βπ£ β πΎ (π§ β (π’ Γ π£) β§ (π’ Γ π£) β π€) β (β¨π΄, π΅β© β π€ β (π€ β (β‘πΉ β π) β βπ’ β π½ βπ£ β πΎ (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π))))) |
42 | 41 | impd 412 |
. . . . 5
β’
(βπ§ β
π€ βπ’ β π½ βπ£ β πΎ (π§ β (π’ Γ π£) β§ (π’ Γ π£) β π€) β ((β¨π΄, π΅β© β π€ β§ π€ β (β‘πΉ β π)) β βπ’ β π½ βπ£ β πΎ (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π)))) |
43 | 26, 42 | syl 17 |
. . . 4
β’ ((π β§ π€ β (π½ Γt πΎ)) β ((β¨π΄, π΅β© β π€ β§ π€ β (β‘πΉ β π)) β βπ’ β π½ βπ£ β πΎ (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π)))) |
44 | 21, 43 | sylbid 240 |
. . 3
β’ ((π β§ π€ β (π½ Γt πΎ)) β ((β¨π΄, π΅β© β π€ β§ (πΉ β π€) β π) β βπ’ β π½ βπ£ β πΎ (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π)))) |
45 | 44 | rexlimdva 3149 |
. 2
β’ (π β (βπ€ β (π½ Γt πΎ)(β¨π΄, π΅β© β π€ β§ (πΉ β π€) β π) β βπ’ β π½ βπ£ β πΎ (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π)))) |
46 | 7, 45 | mpd 15 |
1
β’ (π β βπ’ β π½ βπ£ β πΎ (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π))) |