Step | Hyp | Ref
| Expression |
1 | | ssun1 4133 |
. . 3
β’ βͺ ran ((,) β πΉ) β (βͺ ran
((,) β πΉ) βͺ
((1st β ran πΉ) βͺ (2nd β ran πΉ))) |
2 | | uniioombl.1 |
. . . . . . . 8
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
3 | | ovolfcl 24833 |
. . . . . . . 8
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β ((1st
β(πΉβπ₯)) β β β§
(2nd β(πΉβπ₯)) β β β§ (1st
β(πΉβπ₯)) β€ (2nd
β(πΉβπ₯)))) |
4 | 2, 3 | sylan 581 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ((1st
β(πΉβπ₯)) β β β§
(2nd β(πΉβπ₯)) β β β§ (1st
β(πΉβπ₯)) β€ (2nd
β(πΉβπ₯)))) |
5 | | rexr 11202 |
. . . . . . . 8
β’
((1st β(πΉβπ₯)) β β β (1st
β(πΉβπ₯)) β
β*) |
6 | | rexr 11202 |
. . . . . . . 8
β’
((2nd β(πΉβπ₯)) β β β (2nd
β(πΉβπ₯)) β
β*) |
7 | | id 22 |
. . . . . . . 8
β’
((1st β(πΉβπ₯)) β€ (2nd β(πΉβπ₯)) β (1st β(πΉβπ₯)) β€ (2nd β(πΉβπ₯))) |
8 | | prunioo 13399 |
. . . . . . . 8
β’
(((1st β(πΉβπ₯)) β β* β§
(2nd β(πΉβπ₯)) β β* β§
(1st β(πΉβπ₯)) β€ (2nd β(πΉβπ₯))) β (((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯))) βͺ {(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))}) = ((1st β(πΉβπ₯))[,](2nd β(πΉβπ₯)))) |
9 | 5, 6, 7, 8 | syl3an 1161 |
. . . . . . 7
β’
(((1st β(πΉβπ₯)) β β β§ (2nd
β(πΉβπ₯)) β β β§
(1st β(πΉβπ₯)) β€ (2nd β(πΉβπ₯))) β (((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯))) βͺ {(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))}) = ((1st β(πΉβπ₯))[,](2nd β(πΉβπ₯)))) |
10 | 4, 9 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β β) β (((1st
β(πΉβπ₯))(,)(2nd
β(πΉβπ₯))) βͺ {(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))}) = ((1st
β(πΉβπ₯))[,](2nd
β(πΉβπ₯)))) |
11 | | fvco3 6941 |
. . . . . . . . 9
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (((,) β πΉ)βπ₯) = ((,)β(πΉβπ₯))) |
12 | 2, 11 | sylan 581 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (((,) β πΉ)βπ₯) = ((,)β(πΉβπ₯))) |
13 | 2 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β (πΉβπ₯) β ( β€ β© (β Γ
β))) |
14 | 13 | elin2d 4160 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β (πΉβπ₯) β (β Γ
β)) |
15 | | 1st2nd2 7961 |
. . . . . . . . . . 11
β’ ((πΉβπ₯) β (β Γ β) β
(πΉβπ₯) = β¨(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))β©) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (πΉβπ₯) = β¨(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))β©) |
17 | 16 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((,)β(πΉβπ₯)) = ((,)ββ¨(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))β©)) |
18 | | df-ov 7361 |
. . . . . . . . 9
β’
((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯))) = ((,)ββ¨(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))β©) |
19 | 17, 18 | eqtr4di 2795 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ((,)β(πΉβπ₯)) = ((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯)))) |
20 | 12, 19 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (((,) β πΉ)βπ₯) = ((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯)))) |
21 | | df-pr 4590 |
. . . . . . . 8
β’
{((1st β πΉ)βπ₯), ((2nd β πΉ)βπ₯)} = ({((1st β πΉ)βπ₯)} βͺ {((2nd β πΉ)βπ₯)}) |
22 | | fvco3 6941 |
. . . . . . . . . 10
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β ((1st
β πΉ)βπ₯) = (1st
β(πΉβπ₯))) |
23 | 2, 22 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((1st
β πΉ)βπ₯) = (1st
β(πΉβπ₯))) |
24 | | fvco3 6941 |
. . . . . . . . . 10
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β ((2nd
β πΉ)βπ₯) = (2nd
β(πΉβπ₯))) |
25 | 2, 24 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((2nd
β πΉ)βπ₯) = (2nd
β(πΉβπ₯))) |
26 | 23, 25 | preq12d 4703 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β {((1st
β πΉ)βπ₯), ((2nd β
πΉ)βπ₯)} = {(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))}) |
27 | 21, 26 | eqtr3id 2791 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ({((1st
β πΉ)βπ₯)} βͺ {((2nd
β πΉ)βπ₯)}) = {(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))}) |
28 | 20, 27 | uneq12d 4125 |
. . . . . 6
β’ ((π β§ π₯ β β) β ((((,) β πΉ)βπ₯) βͺ ({((1st β πΉ)βπ₯)} βͺ {((2nd β πΉ)βπ₯)})) = (((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯))) βͺ {(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))})) |
29 | | fvco3 6941 |
. . . . . . . 8
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (([,] β πΉ)βπ₯) = ([,]β(πΉβπ₯))) |
30 | 2, 29 | sylan 581 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (([,] β πΉ)βπ₯) = ([,]β(πΉβπ₯))) |
31 | 16 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ([,]β(πΉβπ₯)) = ([,]ββ¨(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))β©)) |
32 | | df-ov 7361 |
. . . . . . . 8
β’
((1st β(πΉβπ₯))[,](2nd β(πΉβπ₯))) = ([,]ββ¨(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))β©) |
33 | 31, 32 | eqtr4di 2795 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ([,]β(πΉβπ₯)) = ((1st β(πΉβπ₯))[,](2nd β(πΉβπ₯)))) |
34 | 30, 33 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π₯ β β) β (([,] β πΉ)βπ₯) = ((1st β(πΉβπ₯))[,](2nd β(πΉβπ₯)))) |
35 | 10, 28, 34 | 3eqtr4rd 2788 |
. . . . 5
β’ ((π β§ π₯ β β) β (([,] β πΉ)βπ₯) = ((((,) β πΉ)βπ₯) βͺ ({((1st β πΉ)βπ₯)} βͺ {((2nd β πΉ)βπ₯)}))) |
36 | 35 | iuneq2dv 4979 |
. . . 4
β’ (π β βͺ π₯ β β (([,] β πΉ)βπ₯) = βͺ π₯ β β ((((,) β
πΉ)βπ₯) βͺ ({((1st β πΉ)βπ₯)} βͺ {((2nd β πΉ)βπ₯)}))) |
37 | | iccf 13366 |
. . . . . . 7
β’
[,]:(β* Γ β*)βΆπ«
β* |
38 | | ffn 6669 |
. . . . . . 7
β’
([,]:(β* Γ β*)βΆπ«
β* β [,] Fn (β* Γ
β*)) |
39 | 37, 38 | ax-mp 5 |
. . . . . 6
β’ [,] Fn
(β* Γ β*) |
40 | | inss2 4190 |
. . . . . . . 8
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
41 | | rexpssxrxp 11201 |
. . . . . . . 8
β’ (β
Γ β) β (β* Γ
β*) |
42 | 40, 41 | sstri 3954 |
. . . . . . 7
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
43 | | fss 6686 |
. . . . . . 7
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΉ:ββΆ(β* Γ
β*)) |
44 | 2, 42, 43 | sylancl 587 |
. . . . . 6
β’ (π β πΉ:ββΆ(β* Γ
β*)) |
45 | | fnfco 6708 |
. . . . . 6
β’ (([,] Fn
(β* Γ β*) β§ πΉ:ββΆ(β* Γ
β*)) β ([,] β πΉ) Fn β) |
46 | 39, 44, 45 | sylancr 588 |
. . . . 5
β’ (π β ([,] β πΉ) Fn β) |
47 | | fniunfv 7195 |
. . . . 5
β’ (([,]
β πΉ) Fn β
β βͺ π₯ β β (([,] β πΉ)βπ₯) = βͺ ran ([,]
β πΉ)) |
48 | 46, 47 | syl 17 |
. . . 4
β’ (π β βͺ π₯ β β (([,] β πΉ)βπ₯) = βͺ ran ([,]
β πΉ)) |
49 | | iunun 5054 |
. . . . 5
β’ βͺ π₯ β β ((((,) β πΉ)βπ₯) βͺ ({((1st β πΉ)βπ₯)} βͺ {((2nd β πΉ)βπ₯)})) = (βͺ
π₯ β β (((,)
β πΉ)βπ₯) βͺ βͺ π₯ β β ({((1st β
πΉ)βπ₯)} βͺ {((2nd β πΉ)βπ₯)})) |
50 | | ioof 13365 |
. . . . . . . . 9
β’
(,):(β* Γ β*)βΆπ«
β |
51 | | ffn 6669 |
. . . . . . . . 9
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . 8
β’ (,) Fn
(β* Γ β*) |
53 | | fnfco 6708 |
. . . . . . . 8
β’ (((,) Fn
(β* Γ β*) β§ πΉ:ββΆ(β* Γ
β*)) β ((,) β πΉ) Fn β) |
54 | 52, 44, 53 | sylancr 588 |
. . . . . . 7
β’ (π β ((,) β πΉ) Fn β) |
55 | | fniunfv 7195 |
. . . . . . 7
β’ (((,)
β πΉ) Fn β
β βͺ π₯ β β (((,) β πΉ)βπ₯) = βͺ ran ((,)
β πΉ)) |
56 | 54, 55 | syl 17 |
. . . . . 6
β’ (π β βͺ π₯ β β (((,) β πΉ)βπ₯) = βͺ ran ((,)
β πΉ)) |
57 | | iunun 5054 |
. . . . . . 7
β’ βͺ π₯ β β ({((1st β
πΉ)βπ₯)} βͺ {((2nd β πΉ)βπ₯)}) = (βͺ
π₯ β β
{((1st β πΉ)βπ₯)} βͺ βͺ
π₯ β β
{((2nd β πΉ)βπ₯)}) |
58 | | fo1st 7942 |
. . . . . . . . . . . . . 14
β’
1st :VβontoβV |
59 | | fofn 6759 |
. . . . . . . . . . . . . 14
β’
(1st :VβontoβV β 1st Fn V) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
1st Fn V |
61 | | ssv 3969 |
. . . . . . . . . . . . . 14
β’ ( β€
β© (β Γ β)) β V |
62 | | fss 6686 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β V) β πΉ:ββΆV) |
63 | 2, 61, 62 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β πΉ:ββΆV) |
64 | | fnfco 6708 |
. . . . . . . . . . . . 13
β’
((1st Fn V β§ πΉ:ββΆV) β (1st
β πΉ) Fn
β) |
65 | 60, 63, 64 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β (1st β
πΉ) Fn
β) |
66 | | fnfun 6603 |
. . . . . . . . . . . 12
β’
((1st β πΉ) Fn β β Fun (1st
β πΉ)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . 11
β’ (π β Fun (1st
β πΉ)) |
68 | | fndm 6606 |
. . . . . . . . . . . 12
β’
((1st β πΉ) Fn β β dom (1st
β πΉ) =
β) |
69 | | eqimss2 4002 |
. . . . . . . . . . . 12
β’ (dom
(1st β πΉ)
= β β β β dom (1st β πΉ)) |
70 | 65, 68, 69 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β β β dom
(1st β πΉ)) |
71 | | dfimafn2 6907 |
. . . . . . . . . . 11
β’ ((Fun
(1st β πΉ)
β§ β β dom (1st β πΉ)) β ((1st β πΉ) β β) = βͺ π₯ β β {((1st β
πΉ)βπ₯)}) |
72 | 67, 70, 71 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β ((1st β
πΉ) β β) =
βͺ π₯ β β {((1st β
πΉ)βπ₯)}) |
73 | | fnima 6632 |
. . . . . . . . . . 11
β’
((1st β πΉ) Fn β β ((1st β
πΉ) β β) = ran
(1st β πΉ)) |
74 | 65, 73 | syl 17 |
. . . . . . . . . 10
β’ (π β ((1st β
πΉ) β β) = ran
(1st β πΉ)) |
75 | 72, 74 | eqtr3d 2779 |
. . . . . . . . 9
β’ (π β βͺ π₯ β β {((1st β
πΉ)βπ₯)} = ran (1st β πΉ)) |
76 | | rnco2 6206 |
. . . . . . . . 9
β’ ran
(1st β πΉ)
= (1st β ran πΉ) |
77 | 75, 76 | eqtrdi 2793 |
. . . . . . . 8
β’ (π β βͺ π₯ β β {((1st β
πΉ)βπ₯)} = (1st β ran πΉ)) |
78 | | fo2nd 7943 |
. . . . . . . . . . . . . 14
β’
2nd :VβontoβV |
79 | | fofn 6759 |
. . . . . . . . . . . . . 14
β’
(2nd :VβontoβV β 2nd Fn V) |
80 | 78, 79 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
2nd Fn V |
81 | | fnfco 6708 |
. . . . . . . . . . . . 13
β’
((2nd Fn V β§ πΉ:ββΆV) β (2nd
β πΉ) Fn
β) |
82 | 80, 63, 81 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β (2nd β
πΉ) Fn
β) |
83 | | fnfun 6603 |
. . . . . . . . . . . 12
β’
((2nd β πΉ) Fn β β Fun (2nd
β πΉ)) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
β’ (π β Fun (2nd
β πΉ)) |
85 | | fndm 6606 |
. . . . . . . . . . . 12
β’
((2nd β πΉ) Fn β β dom (2nd
β πΉ) =
β) |
86 | | eqimss2 4002 |
. . . . . . . . . . . 12
β’ (dom
(2nd β πΉ)
= β β β β dom (2nd β πΉ)) |
87 | 82, 85, 86 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β β β dom
(2nd β πΉ)) |
88 | | dfimafn2 6907 |
. . . . . . . . . . 11
β’ ((Fun
(2nd β πΉ)
β§ β β dom (2nd β πΉ)) β ((2nd β πΉ) β β) = βͺ π₯ β β {((2nd β
πΉ)βπ₯)}) |
89 | 84, 87, 88 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β ((2nd β
πΉ) β β) =
βͺ π₯ β β {((2nd β
πΉ)βπ₯)}) |
90 | | fnima 6632 |
. . . . . . . . . . 11
β’
((2nd β πΉ) Fn β β ((2nd β
πΉ) β β) = ran
(2nd β πΉ)) |
91 | 82, 90 | syl 17 |
. . . . . . . . . 10
β’ (π β ((2nd β
πΉ) β β) = ran
(2nd β πΉ)) |
92 | 89, 91 | eqtr3d 2779 |
. . . . . . . . 9
β’ (π β βͺ π₯ β β {((2nd β
πΉ)βπ₯)} = ran (2nd β πΉ)) |
93 | | rnco2 6206 |
. . . . . . . . 9
β’ ran
(2nd β πΉ)
= (2nd β ran πΉ) |
94 | 92, 93 | eqtrdi 2793 |
. . . . . . . 8
β’ (π β βͺ π₯ β β {((2nd β
πΉ)βπ₯)} = (2nd β ran πΉ)) |
95 | 77, 94 | uneq12d 4125 |
. . . . . . 7
β’ (π β (βͺ π₯ β β {((1st β
πΉ)βπ₯)} βͺ βͺ
π₯ β β
{((2nd β πΉ)βπ₯)}) = ((1st β ran πΉ) βͺ (2nd β
ran πΉ))) |
96 | 57, 95 | eqtrid 2789 |
. . . . . 6
β’ (π β βͺ π₯ β β ({((1st β
πΉ)βπ₯)} βͺ {((2nd β πΉ)βπ₯)}) = ((1st β ran πΉ) βͺ (2nd β
ran πΉ))) |
97 | 56, 96 | uneq12d 4125 |
. . . . 5
β’ (π β (βͺ π₯ β β (((,) β πΉ)βπ₯) βͺ βͺ
π₯ β β
({((1st β πΉ)βπ₯)} βͺ {((2nd β πΉ)βπ₯)})) = (βͺ ran ((,)
β πΉ) βͺ
((1st β ran πΉ) βͺ (2nd β ran πΉ)))) |
98 | 49, 97 | eqtrid 2789 |
. . . 4
β’ (π β βͺ π₯ β β ((((,) β πΉ)βπ₯) βͺ ({((1st β πΉ)βπ₯)} βͺ {((2nd β πΉ)βπ₯)})) = (βͺ ran ((,)
β πΉ) βͺ
((1st β ran πΉ) βͺ (2nd β ran πΉ)))) |
99 | 36, 48, 98 | 3eqtr3d 2785 |
. . 3
β’ (π β βͺ ran ([,] β πΉ) = (βͺ ran ((,)
β πΉ) βͺ
((1st β ran πΉ) βͺ (2nd β ran πΉ)))) |
100 | 1, 99 | sseqtrrid 3998 |
. 2
β’ (π β βͺ ran ((,) β πΉ) β βͺ ran
([,] β πΉ)) |
101 | | ovolficcss 24836 |
. . . . 5
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β βͺ ran ([,] β
πΉ) β
β) |
102 | 2, 101 | syl 17 |
. . . 4
β’ (π β βͺ ran ([,] β πΉ) β β) |
103 | 102 | ssdifssd 4103 |
. . 3
β’ (π β (βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) β
β) |
104 | | omelon 9583 |
. . . . . . . . . . 11
β’ Ο
β On |
105 | | nnenom 13886 |
. . . . . . . . . . . 12
β’ β
β Ο |
106 | 105 | ensymi 8945 |
. . . . . . . . . . 11
β’ Ο
β β |
107 | | isnumi 9883 |
. . . . . . . . . . 11
β’ ((Ο
β On β§ Ο β β) β β β dom
card) |
108 | 104, 106,
107 | mp2an 691 |
. . . . . . . . . 10
β’ β
β dom card |
109 | | fofun 6758 |
. . . . . . . . . . . . 13
β’
(1st :VβontoβV β Fun 1st ) |
110 | 58, 109 | ax-mp 5 |
. . . . . . . . . . . 12
β’ Fun
1st |
111 | | ssv 3969 |
. . . . . . . . . . . . 13
β’ ran πΉ β V |
112 | | fof 6757 |
. . . . . . . . . . . . . . 15
β’
(1st :VβontoβV β 1st
:VβΆV) |
113 | 58, 112 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
1st :VβΆV |
114 | 113 | fdmi 6681 |
. . . . . . . . . . . . 13
β’ dom
1st = V |
115 | 111, 114 | sseqtrri 3982 |
. . . . . . . . . . . 12
β’ ran πΉ β dom
1st |
116 | | fores 6767 |
. . . . . . . . . . . 12
β’ ((Fun
1st β§ ran πΉ
β dom 1st ) β (1st βΎ ran πΉ):ran πΉβontoβ(1st β ran πΉ)) |
117 | 110, 115,
116 | mp2an 691 |
. . . . . . . . . . 11
β’
(1st βΎ ran πΉ):ran πΉβontoβ(1st β ran πΉ) |
118 | 2 | ffnd 6670 |
. . . . . . . . . . . 12
β’ (π β πΉ Fn β) |
119 | | dffn4 6763 |
. . . . . . . . . . . 12
β’ (πΉ Fn β β πΉ:ββontoβran πΉ) |
120 | 118, 119 | sylib 217 |
. . . . . . . . . . 11
β’ (π β πΉ:ββontoβran πΉ) |
121 | | foco 6771 |
. . . . . . . . . . 11
β’
(((1st βΎ ran πΉ):ran πΉβontoβ(1st β ran πΉ) β§ πΉ:ββontoβran πΉ) β ((1st βΎ ran πΉ) β πΉ):ββontoβ(1st β ran πΉ)) |
122 | 117, 120,
121 | sylancr 588 |
. . . . . . . . . 10
β’ (π β ((1st βΎ
ran πΉ) β πΉ):ββontoβ(1st β ran πΉ)) |
123 | | fodomnum 9994 |
. . . . . . . . . 10
β’ (β
β dom card β (((1st βΎ ran πΉ) β πΉ):ββontoβ(1st β ran πΉ) β (1st β ran πΉ) βΌ
β)) |
124 | 108, 122,
123 | mpsyl 68 |
. . . . . . . . 9
β’ (π β (1st β
ran πΉ) βΌ
β) |
125 | | domentr 8954 |
. . . . . . . . 9
β’
(((1st β ran πΉ) βΌ β β§ β β
Ο) β (1st β ran πΉ) βΌ Ο) |
126 | 124, 105,
125 | sylancl 587 |
. . . . . . . 8
β’ (π β (1st β
ran πΉ) βΌ
Ο) |
127 | | fofun 6758 |
. . . . . . . . . . . . 13
β’
(2nd :VβontoβV β Fun 2nd ) |
128 | 78, 127 | ax-mp 5 |
. . . . . . . . . . . 12
β’ Fun
2nd |
129 | | fof 6757 |
. . . . . . . . . . . . . . 15
β’
(2nd :VβontoβV β 2nd
:VβΆV) |
130 | 78, 129 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
2nd :VβΆV |
131 | 130 | fdmi 6681 |
. . . . . . . . . . . . 13
β’ dom
2nd = V |
132 | 111, 131 | sseqtrri 3982 |
. . . . . . . . . . . 12
β’ ran πΉ β dom
2nd |
133 | | fores 6767 |
. . . . . . . . . . . 12
β’ ((Fun
2nd β§ ran πΉ
β dom 2nd ) β (2nd βΎ ran πΉ):ran πΉβontoβ(2nd β ran πΉ)) |
134 | 128, 132,
133 | mp2an 691 |
. . . . . . . . . . 11
β’
(2nd βΎ ran πΉ):ran πΉβontoβ(2nd β ran πΉ) |
135 | | foco 6771 |
. . . . . . . . . . 11
β’
(((2nd βΎ ran πΉ):ran πΉβontoβ(2nd β ran πΉ) β§ πΉ:ββontoβran πΉ) β ((2nd βΎ ran πΉ) β πΉ):ββontoβ(2nd β ran πΉ)) |
136 | 134, 120,
135 | sylancr 588 |
. . . . . . . . . 10
β’ (π β ((2nd βΎ
ran πΉ) β πΉ):ββontoβ(2nd β ran πΉ)) |
137 | | fodomnum 9994 |
. . . . . . . . . 10
β’ (β
β dom card β (((2nd βΎ ran πΉ) β πΉ):ββontoβ(2nd β ran πΉ) β (2nd β ran πΉ) βΌ
β)) |
138 | 108, 136,
137 | mpsyl 68 |
. . . . . . . . 9
β’ (π β (2nd β
ran πΉ) βΌ
β) |
139 | | domentr 8954 |
. . . . . . . . 9
β’
(((2nd β ran πΉ) βΌ β β§ β β
Ο) β (2nd β ran πΉ) βΌ Ο) |
140 | 138, 105,
139 | sylancl 587 |
. . . . . . . 8
β’ (π β (2nd β
ran πΉ) βΌ
Ο) |
141 | | unctb 10142 |
. . . . . . . 8
β’
(((1st β ran πΉ) βΌ Ο β§ (2nd
β ran πΉ) βΌ
Ο) β ((1st β ran πΉ) βͺ (2nd β ran πΉ)) βΌ
Ο) |
142 | 126, 140,
141 | syl2anc 585 |
. . . . . . 7
β’ (π β ((1st β
ran πΉ) βͺ
(2nd β ran πΉ)) βΌ Ο) |
143 | | ctex 8904 |
. . . . . . 7
β’
(((1st β ran πΉ) βͺ (2nd β ran πΉ)) βΌ Ο β
((1st β ran πΉ) βͺ (2nd β ran πΉ)) β V) |
144 | 142, 143 | syl 17 |
. . . . . 6
β’ (π β ((1st β
ran πΉ) βͺ
(2nd β ran πΉ)) β V) |
145 | | ssid 3967 |
. . . . . . . 8
β’ βͺ ran ([,] β πΉ) β βͺ ran
([,] β πΉ) |
146 | 145, 99 | sseqtrid 3997 |
. . . . . . 7
β’ (π β βͺ ran ([,] β πΉ) β (βͺ ran
((,) β πΉ) βͺ
((1st β ran πΉ) βͺ (2nd β ran πΉ)))) |
147 | | ssundif 4446 |
. . . . . . 7
β’ (βͺ ran ([,] β πΉ) β (βͺ ran
((,) β πΉ) βͺ
((1st β ran πΉ) βͺ (2nd β ran πΉ))) β (βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) β
((1st β ran πΉ) βͺ (2nd β ran πΉ))) |
148 | 146, 147 | sylib 217 |
. . . . . 6
β’ (π β (βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) β
((1st β ran πΉ) βͺ (2nd β ran πΉ))) |
149 | | ssdomg 8941 |
. . . . . 6
β’
(((1st β ran πΉ) βͺ (2nd β ran πΉ)) β V β ((βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) β
((1st β ran πΉ) βͺ (2nd β ran πΉ)) β (βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) βΌ
((1st β ran πΉ) βͺ (2nd β ran πΉ)))) |
150 | 144, 148,
149 | sylc 65 |
. . . . 5
β’ (π β (βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) βΌ
((1st β ran πΉ) βͺ (2nd β ran πΉ))) |
151 | | domtr 8948 |
. . . . 5
β’ (((βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) βΌ
((1st β ran πΉ) βͺ (2nd β ran πΉ)) β§ ((1st
β ran πΉ) βͺ
(2nd β ran πΉ)) βΌ Ο) β (βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) βΌ
Ο) |
152 | 150, 142,
151 | syl2anc 585 |
. . . 4
β’ (π β (βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) βΌ
Ο) |
153 | | domentr 8954 |
. . . 4
β’ (((βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) βΌ
Ο β§ Ο β β) β (βͺ ran
([,] β πΉ) β
βͺ ran ((,) β πΉ)) βΌ β) |
154 | 152, 106,
153 | sylancl 587 |
. . 3
β’ (π β (βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) βΌ
β) |
155 | | ovolctb2 24859 |
. . 3
β’ (((βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) β
β β§ (βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ)) βΌ
β) β (vol*β(βͺ ran ([,] β
πΉ) β βͺ ran ((,) β πΉ))) = 0) |
156 | 103, 154,
155 | syl2anc 585 |
. 2
β’ (π β (vol*β(βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ))) =
0) |
157 | 100, 156 | jca 513 |
1
β’ (π β (βͺ ran ((,) β πΉ) β βͺ ran
([,] β πΉ) β§
(vol*β(βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ))) =
0)) |