Step | Hyp | Ref
| Expression |
1 | | vex 3452 |
. . . . . . 7
β’ π β V |
2 | 1 | dmex 7853 |
. . . . . 6
β’ dom π β V |
3 | 2 | a1i 11 |
. . . . 5
β’
((CHOICE β§ π:dom πβΆComp) β dom π β V) |
4 | | simpr 486 |
. . . . 5
β’
((CHOICE β§ π:dom πβΆComp) β π:dom πβΆComp) |
5 | | fvex 6860 |
. . . . . . . 8
β’
(βtβπ) β V |
6 | 5 | uniex 7683 |
. . . . . . 7
β’ βͺ (βtβπ) β V |
7 | | acufl 23284 |
. . . . . . . 8
β’
(CHOICE β UFL = V) |
8 | 7 | adantr 482 |
. . . . . . 7
β’
((CHOICE β§ π:dom πβΆComp) β UFL =
V) |
9 | 6, 8 | eleqtrrid 2845 |
. . . . . 6
β’
((CHOICE β§ π:dom πβΆComp) β βͺ (βtβπ) β UFL) |
10 | | simpl 484 |
. . . . . . . 8
β’
((CHOICE β§ π:dom πβΆComp) β
CHOICE) |
11 | | dfac10 10080 |
. . . . . . . 8
β’
(CHOICE β dom card = V) |
12 | 10, 11 | sylib 217 |
. . . . . . 7
β’
((CHOICE β§ π:dom πβΆComp) β dom card =
V) |
13 | 6, 12 | eleqtrrid 2845 |
. . . . . 6
β’
((CHOICE β§ π:dom πβΆComp) β βͺ (βtβπ) β dom card) |
14 | 9, 13 | elind 4159 |
. . . . 5
β’
((CHOICE β§ π:dom πβΆComp) β βͺ (βtβπ) β (UFL β© dom
card)) |
15 | | eqid 2737 |
. . . . . 6
β’
(βtβπ) = (βtβπ) |
16 | | eqid 2737 |
. . . . . 6
β’ βͺ (βtβπ) = βͺ
(βtβπ) |
17 | 15, 16 | ptcmpg 23424 |
. . . . 5
β’ ((dom
π β V β§ π:dom πβΆComp β§ βͺ (βtβπ) β (UFL β© dom card)) β
(βtβπ) β Comp) |
18 | 3, 4, 14, 17 | syl3anc 1372 |
. . . 4
β’
((CHOICE β§ π:dom πβΆComp) β
(βtβπ) β Comp) |
19 | 18 | ex 414 |
. . 3
β’
(CHOICE β (π:dom πβΆComp β
(βtβπ) β Comp)) |
20 | 19 | alrimiv 1931 |
. 2
β’
(CHOICE β βπ(π:dom πβΆComp β
(βtβπ) β Comp)) |
21 | | fvex 6860 |
. . . . . . . . 9
β’ (πβπ¦) β V |
22 | | kelac2lem 41420 |
. . . . . . . . 9
β’ ((πβπ¦) β V β (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}) β Comp) |
23 | 21, 22 | mp1i 13 |
. . . . . . . 8
β’ (((Fun
π β§ β
β ran
π) β§ π¦ β dom π) β (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}) β Comp) |
24 | 23 | fmpttd 7068 |
. . . . . . 7
β’ ((Fun
π β§ β
β ran
π) β (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})):dom πβΆComp) |
25 | 24 | ffdmd 6704 |
. . . . . 6
β’ ((Fun
π β§ β
β ran
π) β (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})):dom (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))βΆComp) |
26 | | vex 3452 |
. . . . . . . . 9
β’ π β V |
27 | 26 | dmex 7853 |
. . . . . . . 8
β’ dom π β V |
28 | 27 | mptex 7178 |
. . . . . . 7
β’ (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})) β V |
29 | | id 22 |
. . . . . . . . 9
β’ (π = (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})) β π = (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) |
30 | | dmeq 5864 |
. . . . . . . . 9
β’ (π = (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})) β dom π = dom (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) |
31 | 29, 30 | feq12d 6661 |
. . . . . . . 8
β’ (π = (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})) β (π:dom πβΆComp β (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})):dom (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))βΆComp)) |
32 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})) β (βtβπ) =
(βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})))) |
33 | 32 | eleq1d 2823 |
. . . . . . . 8
β’ (π = (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})) β ((βtβπ) β Comp β
(βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp)) |
34 | 31, 33 | imbi12d 345 |
. . . . . . 7
β’ (π = (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})) β ((π:dom πβΆComp β
(βtβπ) β Comp) β ((π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})):dom (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))βΆComp β
(βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp))) |
35 | 28, 34 | spcv 3567 |
. . . . . 6
β’
(βπ(π:dom πβΆComp β
(βtβπ) β Comp) β ((π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})):dom (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))βΆComp β
(βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp)) |
36 | 25, 35 | syl5com 31 |
. . . . 5
β’ ((Fun
π β§ β
β ran
π) β (βπ(π:dom πβΆComp β
(βtβπ) β Comp) β
(βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp)) |
37 | | fvex 6860 |
. . . . . . . 8
β’ (πβπ₯) β V |
38 | 37 | a1i 11 |
. . . . . . 7
β’ ((((Fun
π β§ β
β ran
π) β§
(βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp) β§ π₯ β dom π) β (πβπ₯) β V) |
39 | | df-nel 3051 |
. . . . . . . . . . 11
β’ (β
β ran π β Β¬
β
β ran π) |
40 | 39 | biimpi 215 |
. . . . . . . . . 10
β’ (β
β ran π β Β¬
β
β ran π) |
41 | 40 | ad2antlr 726 |
. . . . . . . . 9
β’ (((Fun
π β§ β
β ran
π) β§ π₯ β dom π) β Β¬ β
β ran π) |
42 | | fvelrn 7032 |
. . . . . . . . . . . 12
β’ ((Fun
π β§ π₯ β dom π) β (πβπ₯) β ran π) |
43 | 42 | adantlr 714 |
. . . . . . . . . . 11
β’ (((Fun
π β§ β
β ran
π) β§ π₯ β dom π) β (πβπ₯) β ran π) |
44 | | eleq1 2826 |
. . . . . . . . . . 11
β’ ((πβπ₯) = β
β ((πβπ₯) β ran π β β
β ran π)) |
45 | 43, 44 | syl5ibcom 244 |
. . . . . . . . . 10
β’ (((Fun
π β§ β
β ran
π) β§ π₯ β dom π) β ((πβπ₯) = β
β β
β ran π)) |
46 | 45 | necon3bd 2958 |
. . . . . . . . 9
β’ (((Fun
π β§ β
β ran
π) β§ π₯ β dom π) β (Β¬ β
β ran π β (πβπ₯) β β
)) |
47 | 41, 46 | mpd 15 |
. . . . . . . 8
β’ (((Fun
π β§ β
β ran
π) β§ π₯ β dom π) β (πβπ₯) β β
) |
48 | 47 | adantlr 714 |
. . . . . . 7
β’ ((((Fun
π β§ β
β ran
π) β§
(βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp) β§ π₯ β dom π) β (πβπ₯) β β
) |
49 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β (πβπ¦) = (πβπ₯)) |
50 | 49 | unieqd 4884 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β βͺ (πβπ¦) = βͺ (πβπ₯)) |
51 | 50 | pweqd 4582 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β π« βͺ (πβπ¦) = π« βͺ
(πβπ₯)) |
52 | 51 | sneqd 4603 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β {π« βͺ (πβπ¦)} = {π« βͺ
(πβπ₯)}) |
53 | 49, 52 | preq12d 4707 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β {(πβπ¦), {π« βͺ
(πβπ¦)}} = {(πβπ₯), {π« βͺ
(πβπ₯)}}) |
54 | 53 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}) = (topGenβ{(πβπ₯), {π« βͺ
(πβπ₯)}})) |
55 | 54 | cbvmptv 5223 |
. . . . . . . . . . 11
β’ (π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}})) = (π₯ β dom π β¦ (topGenβ{(πβπ₯), {π« βͺ
(πβπ₯)}})) |
56 | 55 | fveq2i 6850 |
. . . . . . . . . 10
β’
(βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) = (βtβ(π₯ β dom π β¦ (topGenβ{(πβπ₯), {π« βͺ
(πβπ₯)}}))) |
57 | 56 | eleq1i 2829 |
. . . . . . . . 9
β’
((βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp β
(βtβ(π₯ β dom π β¦ (topGenβ{(πβπ₯), {π« βͺ
(πβπ₯)}}))) β Comp) |
58 | 57 | biimpi 215 |
. . . . . . . 8
β’
((βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp β
(βtβ(π₯ β dom π β¦ (topGenβ{(πβπ₯), {π« βͺ
(πβπ₯)}}))) β Comp) |
59 | 58 | adantl 483 |
. . . . . . 7
β’ (((Fun
π β§ β
β ran
π) β§
(βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp) β
(βtβ(π₯ β dom π β¦ (topGenβ{(πβπ₯), {π« βͺ
(πβπ₯)}}))) β Comp) |
60 | 38, 48, 59 | kelac2 41421 |
. . . . . 6
β’ (((Fun
π β§ β
β ran
π) β§
(βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp) β Xπ₯ β
dom π(πβπ₯) β β
) |
61 | 60 | ex 414 |
. . . . 5
β’ ((Fun
π β§ β
β ran
π) β
((βtβ(π¦ β dom π β¦ (topGenβ{(πβπ¦), {π« βͺ
(πβπ¦)}}))) β Comp β Xπ₯ β
dom π(πβπ₯) β β
)) |
62 | 36, 61 | syldc 48 |
. . . 4
β’
(βπ(π:dom πβΆComp β
(βtβπ) β Comp) β ((Fun π β§ β
β ran π) β Xπ₯ β
dom π(πβπ₯) β β
)) |
63 | 62 | alrimiv 1931 |
. . 3
β’
(βπ(π:dom πβΆComp β
(βtβπ) β Comp) β βπ((Fun π β§ β
β ran π) β Xπ₯ β dom π(πβπ₯) β β
)) |
64 | | dfac9 10079 |
. . 3
β’
(CHOICE β βπ((Fun π β§ β
β ran π) β Xπ₯ β dom π(πβπ₯) β β
)) |
65 | 63, 64 | sylibr 233 |
. 2
β’
(βπ(π:dom πβΆComp β
(βtβπ) β Comp) β
CHOICE) |
66 | 20, 65 | impbii 208 |
1
β’
(CHOICE β βπ(π:dom πβΆComp β
(βtβπ) β Comp)) |