Step | Hyp | Ref
| Expression |
1 | | opnvonmbllem1.i |
. . . . . 6
β’
β²ππ |
2 | | opnvonmbllem1.c |
. . . . . . . 8
β’ (π β πΆ:πβΆβ) |
3 | 2 | ffvelcdmda 7055 |
. . . . . . 7
β’ ((π β§ π β π) β (πΆβπ) β β) |
4 | | opnvonmbllem1.d |
. . . . . . . 8
β’ (π β π·:πβΆβ) |
5 | 4 | ffvelcdmda 7055 |
. . . . . . 7
β’ ((π β§ π β π) β (π·βπ) β β) |
6 | | opelxpi 5690 |
. . . . . . 7
β’ (((πΆβπ) β β β§ (π·βπ) β β) β β¨(πΆβπ), (π·βπ)β© β (β Γ
β)) |
7 | 3, 5, 6 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π β π) β β¨(πΆβπ), (π·βπ)β© β (β Γ
β)) |
8 | | opnvonmbllem1.h |
. . . . . 6
β’ π» = (π β π β¦ β¨(πΆβπ), (π·βπ)β©) |
9 | 1, 7, 8 | fmptdf 7085 |
. . . . 5
β’ (π β π»:πβΆ(β Γ
β)) |
10 | | qex 12910 |
. . . . . . . . 9
β’ β
β V |
11 | 10, 10 | xpex 7707 |
. . . . . . . 8
β’ (β
Γ β) β V |
12 | 11 | a1i 11 |
. . . . . . 7
β’ (π β (β Γ β)
β V) |
13 | | opnvonmbllem1.x |
. . . . . . 7
β’ (π β π β π) |
14 | 12, 13 | jca 512 |
. . . . . 6
β’ (π β ((β Γ β)
β V β§ π β
π)) |
15 | | elmapg 8800 |
. . . . . 6
β’
(((β Γ β) β V β§ π β π) β (π» β ((β Γ β)
βm π)
β π»:πβΆ(β Γ
β))) |
16 | 14, 15 | syl 17 |
. . . . 5
β’ (π β (π» β ((β Γ β)
βm π)
β π»:πβΆ(β Γ
β))) |
17 | 9, 16 | mpbird 256 |
. . . 4
β’ (π β π» β ((β Γ β)
βm π)) |
18 | 1, 8 | hoi2toco 45001 |
. . . . 5
β’ (π β Xπ β
π (([,) β π»)βπ) = Xπ β π ((πΆβπ)[,)(π·βπ))) |
19 | | opnvonmbllem1.s |
. . . . . 6
β’ (π β Xπ β
π ((πΆβπ)[,)(π·βπ)) β π΅) |
20 | | opnvonmbllem1.g |
. . . . . 6
β’ (π β π΅ β πΊ) |
21 | 19, 20 | sstrd 3972 |
. . . . 5
β’ (π β Xπ β
π ((πΆβπ)[,)(π·βπ)) β πΊ) |
22 | 18, 21 | eqsstrd 4000 |
. . . 4
β’ (π β Xπ β
π (([,) β π»)βπ) β πΊ) |
23 | 17, 22 | jca 512 |
. . 3
β’ (π β (π» β ((β Γ β)
βm π) β§
Xπ
β π (([,) β
π»)βπ) β πΊ)) |
24 | | nfcv 2902 |
. . . . . . 7
β’
β²πβ |
25 | | nfmpt1 5233 |
. . . . . . . 8
β’
β²π(π β π β¦ β¨(πΆβπ), (π·βπ)β©) |
26 | 8, 25 | nfcxfr 2900 |
. . . . . . 7
β’
β²ππ» |
27 | 24, 26 | nfeq 2915 |
. . . . . 6
β’
β²π β = π» |
28 | | coeq2 5834 |
. . . . . . . 8
β’ (β = π» β ([,) β β) = ([,) β π»)) |
29 | 28 | fveq1d 6864 |
. . . . . . 7
β’ (β = π» β (([,) β β)βπ) = (([,) β π»)βπ)) |
30 | 29 | adantr 481 |
. . . . . 6
β’ ((β = π» β§ π β π) β (([,) β β)βπ) = (([,) β π»)βπ)) |
31 | 27, 30 | ixpeq2d 43431 |
. . . . 5
β’ (β = π» β Xπ β π (([,) β β)βπ) = Xπ β π (([,) β π»)βπ)) |
32 | 31 | sseq1d 3993 |
. . . 4
β’ (β = π» β (Xπ β π (([,) β β)βπ) β πΊ β Xπ β π (([,) β π»)βπ) β πΊ)) |
33 | | opnvonmbllem1.k |
. . . 4
β’ πΎ = {β β ((β Γ β)
βm π)
β£ Xπ β π (([,) β β)βπ) β πΊ} |
34 | 32, 33 | elrab2 3666 |
. . 3
β’ (π» β πΎ β (π» β ((β Γ β)
βm π) β§
Xπ
β π (([,) β
π»)βπ) β πΊ)) |
35 | 23, 34 | sylibr 233 |
. 2
β’ (π β π» β πΎ) |
36 | | opnvonmbllem1.y |
. . 3
β’ (π β π β Xπ β π ((πΆβπ)[,)(π·βπ))) |
37 | 36, 18 | eleqtrrd 2835 |
. 2
β’ (π β π β Xπ β π (([,) β π»)βπ)) |
38 | | nfv 1917 |
. . 3
β’
β²β π β Xπ β
π (([,) β π»)βπ) |
39 | | nfcv 2902 |
. . 3
β’
β²βπ» |
40 | | nfrab1 3437 |
. . . 4
β’
β²β{β β ((β Γ
β) βm π) β£ Xπ β π (([,) β β)βπ) β πΊ} |
41 | 33, 40 | nfcxfr 2900 |
. . 3
β’
β²βπΎ |
42 | 31 | eleq2d 2818 |
. . 3
β’ (β = π» β (π β Xπ β π (([,) β β)βπ) β π β Xπ β π (([,) β π»)βπ))) |
43 | 38, 39, 41, 42 | rspcef 43435 |
. 2
β’ ((π» β πΎ β§ π β Xπ β π (([,) β π»)βπ)) β ββ β πΎ π β Xπ β π (([,) β β)βπ)) |
44 | 35, 37, 43 | syl2anc 584 |
1
β’ (π β ββ β πΎ π β Xπ β π (([,) β β)βπ)) |