Step | Hyp | Ref
| Expression |
1 | | ptcnplem.4 |
. . . 4
β’ ((π β§ π) β π β Fin) |
2 | | inss2 4194 |
. . . 4
β’ (πΌ β© π) β π |
3 | | ssfi 9124 |
. . . 4
β’ ((π β Fin β§ (πΌ β© π) β π) β (πΌ β© π) β Fin) |
4 | 1, 2, 3 | sylancl 587 |
. . 3
β’ ((π β§ π) β (πΌ β© π) β Fin) |
5 | | nfv 1918 |
. . . . 5
β’
β²ππ |
6 | | ptcnplem.1 |
. . . . 5
β’
β²ππ |
7 | 5, 6 | nfan 1903 |
. . . 4
β’
β²π(π β§ π) |
8 | | elinel1 4160 |
. . . . . 6
β’ (π β (πΌ β© π) β π β πΌ) |
9 | | ptcnp.7 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (π₯ β π β¦ π΄) β ((π½ CnP (πΉβπ))βπ·)) |
10 | 9 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π) β§ π β πΌ) β (π₯ β π β¦ π΄) β ((π½ CnP (πΉβπ))βπ·)) |
11 | | ptcnplem.3 |
. . . . . . 7
β’ (((π β§ π) β§ π β πΌ) β (πΊβπ) β (πΉβπ)) |
12 | | ptcnp.6 |
. . . . . . . . . . . 12
β’ (π β π· β π) |
13 | 12 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π) β π· β π) |
14 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β πΌ) β§ π₯ β π) β π₯ β π) |
15 | | ptcnp.3 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π½ β (TopOnβπ)) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΌ) β π½ β (TopOnβπ)) |
17 | | ptcnp.5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΉ:πΌβΆTop) |
18 | 17 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΌ) β (πΉβπ) β Top) |
19 | | toptopon2 22283 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉβπ) β Top β (πΉβπ) β (TopOnββͺ (πΉβπ))) |
20 | 18, 19 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΌ) β (πΉβπ) β (TopOnββͺ (πΉβπ))) |
21 | | cnpf2 22617 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ β (TopOnβπ) β§ (πΉβπ) β (TopOnββͺ (πΉβπ)) β§ (π₯ β π β¦ π΄) β ((π½ CnP (πΉβπ))βπ·)) β (π₯ β π β¦ π΄):πβΆβͺ (πΉβπ)) |
22 | 16, 20, 9, 21 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΌ) β (π₯ β π β¦ π΄):πβΆβͺ (πΉβπ)) |
23 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄) |
24 | 23 | fmpt 7063 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ₯ β
π π΄ β βͺ (πΉβπ) β (π₯ β π β¦ π΄):πβΆβͺ (πΉβπ)) |
25 | 22, 24 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β πΌ) β βπ₯ β π π΄ β βͺ (πΉβπ)) |
26 | 25 | r19.21bi 3237 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β πΌ) β§ π₯ β π) β π΄ β βͺ (πΉβπ)) |
27 | 23 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π β§ π΄ β βͺ (πΉβπ)) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
28 | 14, 26, 27 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β πΌ) β§ π₯ β π) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
29 | 28 | an32s 651 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π) β§ π β πΌ) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
30 | 29 | mpteq2dva 5210 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ₯)) = (π β πΌ β¦ π΄)) |
31 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π) β π₯ β π) |
32 | | ptcnp.4 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΌ β π) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π) β πΌ β π) |
34 | 33 | mptexd 7179 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π) β (π β πΌ β¦ π΄) β V) |
35 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π β¦ (π β πΌ β¦ π΄)) = (π₯ β π β¦ (π β πΌ β¦ π΄)) |
36 | 35 | fvmpt2 6964 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π β§ (π β πΌ β¦ π΄) β V) β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) = (π β πΌ β¦ π΄)) |
37 | 31, 34, 36 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) = (π β πΌ β¦ π΄)) |
38 | 30, 37 | eqtr4d 2780 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π) β (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ₯)) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯)) |
39 | 38 | ralrimiva 3144 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β π (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ₯)) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯)) |
40 | 39 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π) β βπ₯ β π (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ₯)) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯)) |
41 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π₯πΌ |
42 | | nffvmpt1 6858 |
. . . . . . . . . . . . . 14
β’
β²π₯((π₯ β π β¦ π΄)βπ·) |
43 | 41, 42 | nfmpt 5217 |
. . . . . . . . . . . . 13
β’
β²π₯(π β πΌ β¦ ((π₯ β π β¦ π΄)βπ·)) |
44 | | nffvmpt1 6858 |
. . . . . . . . . . . . 13
β’
β²π₯((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) |
45 | 43, 44 | nfeq 2921 |
. . . . . . . . . . . 12
β’
β²π₯(π β πΌ β¦ ((π₯ β π β¦ π΄)βπ·)) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) |
46 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π₯ = π· β ((π₯ β π β¦ π΄)βπ₯) = ((π₯ β π β¦ π΄)βπ·)) |
47 | 46 | mpteq2dv 5212 |
. . . . . . . . . . . . 13
β’ (π₯ = π· β (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ₯)) = (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ·))) |
48 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π₯ = π· β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·)) |
49 | 47, 48 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (π₯ = π· β ((π β πΌ β¦ ((π₯ β π β¦ π΄)βπ₯)) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) β (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ·)) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·))) |
50 | 45, 49 | rspc 3572 |
. . . . . . . . . . 11
β’ (π· β π β (βπ₯ β π (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ₯)) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) β (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ·)) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·))) |
51 | 13, 40, 50 | sylc 65 |
. . . . . . . . . 10
β’ ((π β§ π) β (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ·)) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·)) |
52 | | ptcnplem.6 |
. . . . . . . . . 10
β’ ((π β§ π) β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πΊβπ)) |
53 | 51, 52 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((π β§ π) β (π β πΌ β¦ ((π₯ β π β¦ π΄)βπ·)) β Xπ β πΌ (πΊβπ)) |
54 | 32 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π) β πΌ β π) |
55 | | mptelixpg 8880 |
. . . . . . . . . 10
β’ (πΌ β π β ((π β πΌ β¦ ((π₯ β π β¦ π΄)βπ·)) β Xπ β πΌ (πΊβπ) β βπ β πΌ ((π₯ β π β¦ π΄)βπ·) β (πΊβπ))) |
56 | 54, 55 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π) β ((π β πΌ β¦ ((π₯ β π β¦ π΄)βπ·)) β Xπ β πΌ (πΊβπ) β βπ β πΌ ((π₯ β π β¦ π΄)βπ·) β (πΊβπ))) |
57 | 53, 56 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π) β βπ β πΌ ((π₯ β π β¦ π΄)βπ·) β (πΊβπ)) |
58 | 57 | r19.21bi 3237 |
. . . . . . 7
β’ (((π β§ π) β§ π β πΌ) β ((π₯ β π β¦ π΄)βπ·) β (πΊβπ)) |
59 | | cnpimaex 22623 |
. . . . . . 7
β’ (((π₯ β π β¦ π΄) β ((π½ CnP (πΉβπ))βπ·) β§ (πΊβπ) β (πΉβπ) β§ ((π₯ β π β¦ π΄)βπ·) β (πΊβπ)) β βπ’ β π½ (π· β π’ β§ ((π₯ β π β¦ π΄) β π’) β (πΊβπ))) |
60 | 10, 11, 58, 59 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π) β§ π β πΌ) β βπ’ β π½ (π· β π’ β§ ((π₯ β π β¦ π΄) β π’) β (πΊβπ))) |
61 | 8, 60 | sylan2 594 |
. . . . 5
β’ (((π β§ π) β§ π β (πΌ β© π)) β βπ’ β π½ (π· β π’ β§ ((π₯ β π β¦ π΄) β π’) β (πΊβπ))) |
62 | 61 | ex 414 |
. . . 4
β’ ((π β§ π) β (π β (πΌ β© π) β βπ’ β π½ (π· β π’ β§ ((π₯ β π β¦ π΄) β π’) β (πΊβπ)))) |
63 | 7, 62 | ralrimi 3243 |
. . 3
β’ ((π β§ π) β βπ β (πΌ β© π)βπ’ β π½ (π· β π’ β§ ((π₯ β π β¦ π΄) β π’) β (πΊβπ))) |
64 | | eleq2 2827 |
. . . . 5
β’ (π’ = (πβπ) β (π· β π’ β π· β (πβπ))) |
65 | | imaeq2 6014 |
. . . . . 6
β’ (π’ = (πβπ) β ((π₯ β π β¦ π΄) β π’) = ((π₯ β π β¦ π΄) β (πβπ))) |
66 | 65 | sseq1d 3980 |
. . . . 5
β’ (π’ = (πβπ) β (((π₯ β π β¦ π΄) β π’) β (πΊβπ) β ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ))) |
67 | 64, 66 | anbi12d 632 |
. . . 4
β’ (π’ = (πβπ) β ((π· β π’ β§ ((π₯ β π β¦ π΄) β π’) β (πΊβπ)) β (π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) |
68 | 67 | ac6sfi 9238 |
. . 3
β’ (((πΌ β© π) β Fin β§ βπ β (πΌ β© π)βπ’ β π½ (π· β π’ β§ ((π₯ β π β¦ π΄) β π’) β (πΊβπ))) β βπ(π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) |
69 | 4, 63, 68 | syl2anc 585 |
. 2
β’ ((π β§ π) β βπ(π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) |
70 | 15 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β π½ β (TopOnβπ)) |
71 | | toponuni 22279 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
72 | 70, 71 | syl 17 |
. . . . 5
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β π = βͺ π½) |
73 | 72 | ineq1d 4176 |
. . . 4
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β (π β© β© ran
π) = (βͺ π½
β© β© ran π)) |
74 | | topontop 22278 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π½ β Top) |
75 | 15, 74 | syl 17 |
. . . . . 6
β’ (π β π½ β Top) |
76 | 75 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β π½ β Top) |
77 | | frn 6680 |
. . . . . 6
β’ (π:(πΌ β© π)βΆπ½ β ran π β π½) |
78 | 77 | ad2antrl 727 |
. . . . 5
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β ran π β π½) |
79 | 4 | adantr 482 |
. . . . . 6
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β (πΌ β© π) β Fin) |
80 | | ffn 6673 |
. . . . . . . 8
β’ (π:(πΌ β© π)βΆπ½ β π Fn (πΌ β© π)) |
81 | 80 | ad2antrl 727 |
. . . . . . 7
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β π Fn (πΌ β© π)) |
82 | | dffn4 6767 |
. . . . . . 7
β’ (π Fn (πΌ β© π) β π:(πΌ β© π)βontoβran π) |
83 | 81, 82 | sylib 217 |
. . . . . 6
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β π:(πΌ β© π)βontoβran π) |
84 | | fofi 9289 |
. . . . . 6
β’ (((πΌ β© π) β Fin β§ π:(πΌ β© π)βontoβran π) β ran π β Fin) |
85 | 79, 83, 84 | syl2anc 585 |
. . . . 5
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β ran π β Fin) |
86 | | eqid 2737 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
87 | 86 | rintopn 22274 |
. . . . 5
β’ ((π½ β Top β§ ran π β π½ β§ ran π β Fin) β (βͺ π½
β© β© ran π) β π½) |
88 | 76, 78, 85, 87 | syl3anc 1372 |
. . . 4
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β (βͺ
π½ β© β© ran π) β π½) |
89 | 73, 88 | eqeltrd 2838 |
. . 3
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β (π β© β© ran
π) β π½) |
90 | 12 | ad2antrr 725 |
. . . 4
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β π· β π) |
91 | | simpl 484 |
. . . . . . 7
β’ ((π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)) β π· β (πβπ)) |
92 | 91 | ralimi 3087 |
. . . . . 6
β’
(βπ β
(πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)) β βπ β (πΌ β© π)π· β (πβπ)) |
93 | 92 | ad2antll 728 |
. . . . 5
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β βπ β (πΌ β© π)π· β (πβπ)) |
94 | | eleq2 2827 |
. . . . . . 7
β’ (π§ = (πβπ) β (π· β π§ β π· β (πβπ))) |
95 | 94 | ralrn 7043 |
. . . . . 6
β’ (π Fn (πΌ β© π) β (βπ§ β ran π π· β π§ β βπ β (πΌ β© π)π· β (πβπ))) |
96 | 81, 95 | syl 17 |
. . . . 5
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β (βπ§ β ran π π· β π§ β βπ β (πΌ β© π)π· β (πβπ))) |
97 | 93, 96 | mpbird 257 |
. . . 4
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β βπ§ β ran π π· β π§) |
98 | | elrint 4957 |
. . . 4
β’ (π· β (π β© β© ran
π) β (π· β π β§ βπ§ β ran π π· β π§)) |
99 | 90, 97, 98 | sylanbrc 584 |
. . 3
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β π· β (π β© β© ran
π)) |
100 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π π:(πΌ β© π)βΆπ½ |
101 | 7, 100 | nfan 1903 |
. . . . . . . . 9
β’
β²π((π β§ π) β§ π:(πΌ β© π)βΆπ½) |
102 | | funmpt 6544 |
. . . . . . . . . . . . 13
β’ Fun
(π₯ β π β¦ π΄) |
103 | | simp-4l 782 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β π) |
104 | 103, 15 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β π½ β (TopOnβπ)) |
105 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β π:(πΌ β© π)βΆπ½) |
106 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β π β (πΌ β© π)) |
107 | 105, 106 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β (πβπ) β π½) |
108 | | toponss 22292 |
. . . . . . . . . . . . . . 15
β’ ((π½ β (TopOnβπ) β§ (πβπ) β π½) β (πβπ) β π) |
109 | 104, 107,
108 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β (πβπ) β π) |
110 | 106 | elin1d 4163 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β π β πΌ) |
111 | 103, 110,
25 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β βπ₯ β π π΄ β βͺ (πΉβπ)) |
112 | | dmmptg 6199 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
π π΄ β βͺ (πΉβπ) β dom (π₯ β π β¦ π΄) = π) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β dom (π₯ β π β¦ π΄) = π) |
114 | 109, 113 | sseqtrrd 3990 |
. . . . . . . . . . . . 13
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β (πβπ) β dom (π₯ β π β¦ π΄)) |
115 | | funimass4 6912 |
. . . . . . . . . . . . 13
β’ ((Fun
(π₯ β π β¦ π΄) β§ (πβπ) β dom (π₯ β π β¦ π΄)) β (((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ) β βπ‘ β (πβπ)((π₯ β π β¦ π΄)βπ‘) β (πΊβπ))) |
116 | 102, 114,
115 | sylancr 588 |
. . . . . . . . . . . 12
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β (((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ) β βπ‘ β (πβπ)((π₯ β π β¦ π΄)βπ‘) β (πΊβπ))) |
117 | | nffvmpt1 6858 |
. . . . . . . . . . . . . 14
β’
β²π₯((π₯ β π β¦ π΄)βπ‘) |
118 | 117 | nfel1 2924 |
. . . . . . . . . . . . 13
β’
β²π₯((π₯ β π β¦ π΄)βπ‘) β (πΊβπ) |
119 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π‘((π₯ β π β¦ π΄)βπ₯) β (πΊβπ) |
120 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π‘ = π₯ β ((π₯ β π β¦ π΄)βπ‘) = ((π₯ β π β¦ π΄)βπ₯)) |
121 | 120 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π‘ = π₯ β (((π₯ β π β¦ π΄)βπ‘) β (πΊβπ) β ((π₯ β π β¦ π΄)βπ₯) β (πΊβπ))) |
122 | 118, 119,
121 | cbvralw 3292 |
. . . . . . . . . . . 12
β’
(βπ‘ β
(πβπ)((π₯ β π β¦ π΄)βπ‘) β (πΊβπ) β βπ₯ β (πβπ)((π₯ β π β¦ π΄)βπ₯) β (πΊβπ)) |
123 | 116, 122 | bitrdi 287 |
. . . . . . . . . . 11
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β (((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ) β βπ₯ β (πβπ)((π₯ β π β¦ π΄)βπ₯) β (πΊβπ))) |
124 | | inss1 4193 |
. . . . . . . . . . . . 13
β’ (π β© β© ran π) β π |
125 | | ssralv 4015 |
. . . . . . . . . . . . 13
β’ ((π β© β© ran π) β π β (βπ₯ β π π΄ β βͺ (πΉβπ) β βπ₯ β (π β© β© ran
π)π΄ β βͺ (πΉβπ))) |
126 | 124, 111,
125 | mpsyl 68 |
. . . . . . . . . . . 12
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β βπ₯ β (π β© β© ran
π)π΄ β βͺ (πΉβπ)) |
127 | | inss2 4194 |
. . . . . . . . . . . . . 14
β’ (π β© β© ran π) β β© ran
π |
128 | 105, 80 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β π Fn (πΌ β© π)) |
129 | | fnfvelrn 7036 |
. . . . . . . . . . . . . . . 16
β’ ((π Fn (πΌ β© π) β§ π β (πΌ β© π)) β (πβπ) β ran π) |
130 | 128, 106,
129 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β (πβπ) β ran π) |
131 | | intss1 4929 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β ran π β β© ran
π β (πβπ)) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β β© ran
π β (πβπ)) |
133 | 127, 132 | sstrid 3960 |
. . . . . . . . . . . . 13
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β (π β© β© ran
π) β (πβπ)) |
134 | | ssralv 4015 |
. . . . . . . . . . . . 13
β’ ((π β© β© ran π) β (πβπ) β (βπ₯ β (πβπ)((π₯ β π β¦ π΄)βπ₯) β (πΊβπ) β βπ₯ β (π β© β© ran
π)((π₯ β π β¦ π΄)βπ₯) β (πΊβπ))) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . 12
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β (βπ₯ β (πβπ)((π₯ β π β¦ π΄)βπ₯) β (πΊβπ) β βπ₯ β (π β© β© ran
π)((π₯ β π β¦ π΄)βπ₯) β (πΊβπ))) |
136 | | r19.26 3115 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
(π β© β© ran π)(π΄ β βͺ (πΉβπ) β§ ((π₯ β π β¦ π΄)βπ₯) β (πΊβπ)) β (βπ₯ β (π β© β© ran
π)π΄ β βͺ (πΉβπ) β§ βπ₯ β (π β© β© ran
π)((π₯ β π β¦ π΄)βπ₯) β (πΊβπ))) |
137 | | elinel1 4160 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π β© β© ran
π) β π₯ β π) |
138 | 137, 27 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β (π β© β© ran
π) β§ π΄ β βͺ (πΉβπ)) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
139 | 138 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (π β© β© ran
π) β§ π΄ β βͺ (πΉβπ)) β (((π₯ β π β¦ π΄)βπ₯) β (πΊβπ) β π΄ β (πΊβπ))) |
140 | 139 | biimpd 228 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (π β© β© ran
π) β§ π΄ β βͺ (πΉβπ)) β (((π₯ β π β¦ π΄)βπ₯) β (πΊβπ) β π΄ β (πΊβπ))) |
141 | 140 | expimpd 455 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π β© β© ran
π) β ((π΄ β βͺ (πΉβπ) β§ ((π₯ β π β¦ π΄)βπ₯) β (πΊβπ)) β π΄ β (πΊβπ))) |
142 | 141 | ralimia 3084 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
(π β© β© ran π)(π΄ β βͺ (πΉβπ) β§ ((π₯ β π β¦ π΄)βπ₯) β (πΊβπ)) β βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ)) |
143 | 136, 142 | sylbir 234 |
. . . . . . . . . . . 12
β’
((βπ₯ β
(π β© β© ran π)π΄ β βͺ (πΉβπ) β§ βπ₯ β (π β© β© ran
π)((π₯ β π β¦ π΄)βπ₯) β (πΊβπ)) β βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ)) |
144 | 126, 135,
143 | syl6an 683 |
. . . . . . . . . . 11
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β (βπ₯ β (πβπ)((π₯ β π β¦ π΄)βπ₯) β (πΊβπ) β βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ))) |
145 | 123, 144 | sylbid 239 |
. . . . . . . . . 10
β’
(((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β§ π· β (πβπ)) β (((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ) β βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ))) |
146 | 145 | expimpd 455 |
. . . . . . . . 9
β’ ((((π β§ π) β§ π:(πΌ β© π)βΆπ½) β§ π β (πΌ β© π)) β ((π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)) β βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ))) |
147 | 101, 146 | ralimdaa 3246 |
. . . . . . . 8
β’ (((π β§ π) β§ π:(πΌ β© π)βΆπ½) β (βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)) β βπ β (πΌ β© π)βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ))) |
148 | 147 | impr 456 |
. . . . . . 7
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β βπ β (πΌ β© π)βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ)) |
149 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β§ π) β π) |
150 | | eldifi 4091 |
. . . . . . . . . . . 12
β’ (π β (πΌ β π) β π β πΌ) |
151 | 137, 26 | sylan2 594 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΌ) β§ π₯ β (π β© β© ran
π)) β π΄ β βͺ (πΉβπ)) |
152 | 151 | ralrimiva 3144 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β βπ₯ β (π β© β© ran
π)π΄ β βͺ (πΉβπ)) |
153 | 149, 150,
152 | syl2an 597 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β (πΌ β π)) β βπ₯ β (π β© β© ran
π)π΄ β βͺ (πΉβπ)) |
154 | | ptcnplem.5 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (πΌ β π)) β (πΊβπ) = βͺ (πΉβπ)) |
155 | | eleq2 2827 |
. . . . . . . . . . . . 13
β’ ((πΊβπ) = βͺ (πΉβπ) β (π΄ β (πΊβπ) β π΄ β βͺ (πΉβπ))) |
156 | 155 | ralbidv 3175 |
. . . . . . . . . . . 12
β’ ((πΊβπ) = βͺ (πΉβπ) β (βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ) β βπ₯ β (π β© β© ran
π)π΄ β βͺ (πΉβπ))) |
157 | 154, 156 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β (πΌ β π)) β (βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ) β βπ₯ β (π β© β© ran
π)π΄ β βͺ (πΉβπ))) |
158 | 153, 157 | mpbird 257 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β (πΌ β π)) β βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ)) |
159 | 158 | ex 414 |
. . . . . . . . 9
β’ ((π β§ π) β (π β (πΌ β π) β βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ))) |
160 | 7, 159 | ralrimi 3243 |
. . . . . . . 8
β’ ((π β§ π) β βπ β (πΌ β π)βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ)) |
161 | 160 | adantr 482 |
. . . . . . 7
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β βπ β (πΌ β π)βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ)) |
162 | | inundif 4443 |
. . . . . . . . 9
β’ ((πΌ β© π) βͺ (πΌ β π)) = πΌ |
163 | 162 | raleqi 3314 |
. . . . . . . 8
β’
(βπ β
((πΌ β© π) βͺ (πΌ β π))βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ) β βπ β πΌ βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ)) |
164 | | ralunb 4156 |
. . . . . . . 8
β’
(βπ β
((πΌ β© π) βͺ (πΌ β π))βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ) β (βπ β (πΌ β© π)βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ) β§ βπ β (πΌ β π)βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ))) |
165 | 163, 164 | bitr3i 277 |
. . . . . . 7
β’
(βπ β
πΌ βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ) β (βπ β (πΌ β© π)βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ) β§ βπ β (πΌ β π)βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ))) |
166 | 148, 161,
165 | sylanbrc 584 |
. . . . . 6
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β βπ β πΌ βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ)) |
167 | | ralcom 3275 |
. . . . . 6
β’
(βπ₯ β
(π β© β© ran π)βπ β πΌ π΄ β (πΊβπ) β βπ β πΌ βπ₯ β (π β© β© ran
π)π΄ β (πΊβπ)) |
168 | 166, 167 | sylibr 233 |
. . . . 5
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β βπ₯ β (π β© β© ran
π)βπ β πΌ π΄ β (πΊβπ)) |
169 | 32 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β πΌ β π) |
170 | | nffvmpt1 6858 |
. . . . . . . . 9
β’
β²π₯((π₯ β π β¦ (π β πΌ β¦ π΄))βπ‘) |
171 | 170 | nfel1 2924 |
. . . . . . . 8
β’
β²π₯((π₯ β π β¦ (π β πΌ β¦ π΄))βπ‘) β Xπ β πΌ (πΊβπ) |
172 | | nfv 1918 |
. . . . . . . 8
β’
β²π‘((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) β Xπ β πΌ (πΊβπ) |
173 | | fveq2 6847 |
. . . . . . . . 9
β’ (π‘ = π₯ β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ‘) = ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯)) |
174 | 173 | eleq1d 2823 |
. . . . . . . 8
β’ (π‘ = π₯ β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ‘) β Xπ β πΌ (πΊβπ) β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) β Xπ β πΌ (πΊβπ))) |
175 | 171, 172,
174 | cbvralw 3292 |
. . . . . . 7
β’
(βπ‘ β
(π β© β© ran π)((π₯ β π β¦ (π β πΌ β¦ π΄))βπ‘) β Xπ β πΌ (πΊβπ) β βπ₯ β (π β© β© ran
π)((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) β Xπ β πΌ (πΊβπ)) |
176 | | mptexg 7176 |
. . . . . . . . . . 11
β’ (πΌ β π β (π β πΌ β¦ π΄) β V) |
177 | 137, 176,
36 | syl2anr 598 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π₯ β (π β© β© ran
π)) β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) = (π β πΌ β¦ π΄)) |
178 | 177 | eleq1d 2823 |
. . . . . . . . 9
β’ ((πΌ β π β§ π₯ β (π β© β© ran
π)) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) β Xπ β πΌ (πΊβπ) β (π β πΌ β¦ π΄) β Xπ β πΌ (πΊβπ))) |
179 | | mptelixpg 8880 |
. . . . . . . . . 10
β’ (πΌ β π β ((π β πΌ β¦ π΄) β Xπ β πΌ (πΊβπ) β βπ β πΌ π΄ β (πΊβπ))) |
180 | 179 | adantr 482 |
. . . . . . . . 9
β’ ((πΌ β π β§ π₯ β (π β© β© ran
π)) β ((π β πΌ β¦ π΄) β Xπ β πΌ (πΊβπ) β βπ β πΌ π΄ β (πΊβπ))) |
181 | 178, 180 | bitrd 279 |
. . . . . . . 8
β’ ((πΌ β π β§ π₯ β (π β© β© ran
π)) β (((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) β Xπ β πΌ (πΊβπ) β βπ β πΌ π΄ β (πΊβπ))) |
182 | 181 | ralbidva 3173 |
. . . . . . 7
β’ (πΌ β π β (βπ₯ β (π β© β© ran
π)((π₯ β π β¦ (π β πΌ β¦ π΄))βπ₯) β Xπ β πΌ (πΊβπ) β βπ₯ β (π β© β© ran
π)βπ β πΌ π΄ β (πΊβπ))) |
183 | 175, 182 | bitrid 283 |
. . . . . 6
β’ (πΌ β π β (βπ‘ β (π β© β© ran
π)((π₯ β π β¦ (π β πΌ β¦ π΄))βπ‘) β Xπ β πΌ (πΊβπ) β βπ₯ β (π β© β© ran
π)βπ β πΌ π΄ β (πΊβπ))) |
184 | 169, 183 | syl 17 |
. . . . 5
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β (βπ‘ β (π β© β© ran
π)((π₯ β π β¦ (π β πΌ β¦ π΄))βπ‘) β Xπ β πΌ (πΊβπ) β βπ₯ β (π β© β© ran
π)βπ β πΌ π΄ β (πΊβπ))) |
185 | 168, 184 | mpbird 257 |
. . . 4
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β βπ‘ β (π β© β© ran
π)((π₯ β π β¦ (π β πΌ β¦ π΄))βπ‘) β Xπ β πΌ (πΊβπ)) |
186 | | funmpt 6544 |
. . . . 5
β’ Fun
(π₯ β π β¦ (π β πΌ β¦ π΄)) |
187 | 32 | mptexd 7179 |
. . . . . . . . 9
β’ (π β (π β πΌ β¦ π΄) β V) |
188 | 187 | ralrimivw 3148 |
. . . . . . . 8
β’ (π β βπ₯ β π (π β πΌ β¦ π΄) β V) |
189 | 188 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β βπ₯ β π (π β πΌ β¦ π΄) β V) |
190 | | dmmptg 6199 |
. . . . . . 7
β’
(βπ₯ β
π (π β πΌ β¦ π΄) β V β dom (π₯ β π β¦ (π β πΌ β¦ π΄)) = π) |
191 | 189, 190 | syl 17 |
. . . . . 6
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β dom (π₯ β π β¦ (π β πΌ β¦ π΄)) = π) |
192 | 124, 191 | sseqtrrid 4002 |
. . . . 5
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β (π β© β© ran
π) β dom (π₯ β π β¦ (π β πΌ β¦ π΄))) |
193 | | funimass4 6912 |
. . . . 5
β’ ((Fun
(π₯ β π β¦ (π β πΌ β¦ π΄)) β§ (π β© β© ran
π) β dom (π₯ β π β¦ (π β πΌ β¦ π΄))) β (((π₯ β π β¦ (π β πΌ β¦ π΄)) β (π β© β© ran
π)) β Xπ β
πΌ (πΊβπ) β βπ‘ β (π β© β© ran
π)((π₯ β π β¦ (π β πΌ β¦ π΄))βπ‘) β Xπ β πΌ (πΊβπ))) |
194 | 186, 192,
193 | sylancr 588 |
. . . 4
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β (((π₯ β π β¦ (π β πΌ β¦ π΄)) β (π β© β© ran
π)) β Xπ β
πΌ (πΊβπ) β βπ‘ β (π β© β© ran
π)((π₯ β π β¦ (π β πΌ β¦ π΄))βπ‘) β Xπ β πΌ (πΊβπ))) |
195 | 185, 194 | mpbird 257 |
. . 3
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β ((π₯ β π β¦ (π β πΌ β¦ π΄)) β (π β© β© ran
π)) β Xπ β
πΌ (πΊβπ)) |
196 | | eleq2 2827 |
. . . . 5
β’ (π§ = (π β© β© ran
π) β (π· β π§ β π· β (π β© β© ran
π))) |
197 | | imaeq2 6014 |
. . . . . 6
β’ (π§ = (π β© β© ran
π) β ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) = ((π₯ β π β¦ (π β πΌ β¦ π΄)) β (π β© β© ran
π))) |
198 | 197 | sseq1d 3980 |
. . . . 5
β’ (π§ = (π β© β© ran
π) β (((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πΊβπ) β ((π₯ β π β¦ (π β πΌ β¦ π΄)) β (π β© β© ran
π)) β Xπ β
πΌ (πΊβπ))) |
199 | 196, 198 | anbi12d 632 |
. . . 4
β’ (π§ = (π β© β© ran
π) β ((π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πΊβπ)) β (π· β (π β© β© ran
π) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β (π β© β© ran
π)) β Xπ β
πΌ (πΊβπ)))) |
200 | 199 | rspcev 3584 |
. . 3
β’ (((π β© β© ran π) β π½ β§ (π· β (π β© β© ran
π) β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β (π β© β© ran
π)) β Xπ β
πΌ (πΊβπ))) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πΊβπ))) |
201 | 89, 99, 195, 200 | syl12anc 836 |
. 2
β’ (((π β§ π) β§ (π:(πΌ β© π)βΆπ½ β§ βπ β (πΌ β© π)(π· β (πβπ) β§ ((π₯ β π β¦ π΄) β (πβπ)) β (πΊβπ)))) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πΊβπ))) |
202 | 69, 201 | exlimddv 1939 |
1
β’ ((π β§ π) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πΊβπ))) |