Step | Hyp | Ref
| Expression |
1 | | raleq 2672 |
. . . 4
β’ (π’ = β
β (βπ₯ β π’ βπ¦ β π΅ π β βπ₯ β β
βπ¦ β π΅ π)) |
2 | | feq2 5349 |
. . . . . 6
β’ (π’ = β
β (π:π’βΆπ΅ β π:β
βΆπ΅)) |
3 | | raleq 2672 |
. . . . . 6
β’ (π’ = β
β (βπ₯ β π’ π β βπ₯ β β
π)) |
4 | 2, 3 | anbi12d 473 |
. . . . 5
β’ (π’ = β
β ((π:π’βΆπ΅ β§ βπ₯ β π’ π) β (π:β
βΆπ΅ β§ βπ₯ β β
π))) |
5 | 4 | exbidv 1825 |
. . . 4
β’ (π’ = β
β (βπ(π:π’βΆπ΅ β§ βπ₯ β π’ π) β βπ(π:β
βΆπ΅ β§ βπ₯ β β
π))) |
6 | 1, 5 | imbi12d 234 |
. . 3
β’ (π’ = β
β
((βπ₯ β π’ βπ¦ β π΅ π β βπ(π:π’βΆπ΅ β§ βπ₯ β π’ π)) β (βπ₯ β β
βπ¦ β π΅ π β βπ(π:β
βΆπ΅ β§ βπ₯ β β
π)))) |
7 | | raleq 2672 |
. . . 4
β’ (π’ = π€ β (βπ₯ β π’ βπ¦ β π΅ π β βπ₯ β π€ βπ¦ β π΅ π)) |
8 | | feq2 5349 |
. . . . . 6
β’ (π’ = π€ β (π:π’βΆπ΅ β π:π€βΆπ΅)) |
9 | | raleq 2672 |
. . . . . 6
β’ (π’ = π€ β (βπ₯ β π’ π β βπ₯ β π€ π)) |
10 | 8, 9 | anbi12d 473 |
. . . . 5
β’ (π’ = π€ β ((π:π’βΆπ΅ β§ βπ₯ β π’ π) β (π:π€βΆπ΅ β§ βπ₯ β π€ π))) |
11 | 10 | exbidv 1825 |
. . . 4
β’ (π’ = π€ β (βπ(π:π’βΆπ΅ β§ βπ₯ β π’ π) β βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π))) |
12 | 7, 11 | imbi12d 234 |
. . 3
β’ (π’ = π€ β ((βπ₯ β π’ βπ¦ β π΅ π β βπ(π:π’βΆπ΅ β§ βπ₯ β π’ π)) β (βπ₯ β π€ βπ¦ β π΅ π β βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π)))) |
13 | | raleq 2672 |
. . . 4
β’ (π’ = (π€ βͺ {π§}) β (βπ₯ β π’ βπ¦ β π΅ π β βπ₯ β (π€ βͺ {π§})βπ¦ β π΅ π)) |
14 | | feq2 5349 |
. . . . . . 7
β’ (π’ = (π€ βͺ {π§}) β (π:π’βΆπ΅ β π:(π€ βͺ {π§})βΆπ΅)) |
15 | | raleq 2672 |
. . . . . . 7
β’ (π’ = (π€ βͺ {π§}) β (βπ₯ β π’ π β βπ₯ β (π€ βͺ {π§})π)) |
16 | 14, 15 | anbi12d 473 |
. . . . . 6
β’ (π’ = (π€ βͺ {π§}) β ((π:π’βΆπ΅ β§ βπ₯ β π’ π) β (π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})π))) |
17 | 16 | exbidv 1825 |
. . . . 5
β’ (π’ = (π€ βͺ {π§}) β (βπ(π:π’βΆπ΅ β§ βπ₯ β π’ π) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})π))) |
18 | | feq1 5348 |
. . . . . . 7
β’ (π = π β (π:(π€ βͺ {π§})βΆπ΅ β π:(π€ βͺ {π§})βΆπ΅)) |
19 | | vex 2740 |
. . . . . . . . . . 11
β’ π β V |
20 | | vex 2740 |
. . . . . . . . . . 11
β’ π₯ β V |
21 | 19, 20 | fvex 5535 |
. . . . . . . . . 10
β’ (πβπ₯) β V |
22 | | ac6sfi.1 |
. . . . . . . . . 10
β’ (π¦ = (πβπ₯) β (π β π)) |
23 | 21, 22 | sbcie 2997 |
. . . . . . . . 9
β’
([(πβπ₯) / π¦]π β π) |
24 | | fveq1 5514 |
. . . . . . . . . 10
β’ (π = π β (πβπ₯) = (πβπ₯)) |
25 | 24 | sbceq1d 2967 |
. . . . . . . . 9
β’ (π = π β ([(πβπ₯) / π¦]π β [(πβπ₯) / π¦]π)) |
26 | 23, 25 | bitr3id 194 |
. . . . . . . 8
β’ (π = π β (π β [(πβπ₯) / π¦]π)) |
27 | 26 | ralbidv 2477 |
. . . . . . 7
β’ (π = π β (βπ₯ β (π€ βͺ {π§})π β βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)) |
28 | 18, 27 | anbi12d 473 |
. . . . . 6
β’ (π = π β ((π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})π) β (π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π))) |
29 | 28 | cbvexv 1918 |
. . . . 5
β’
(βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})π) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)) |
30 | 17, 29 | bitrdi 196 |
. . . 4
β’ (π’ = (π€ βͺ {π§}) β (βπ(π:π’βΆπ΅ β§ βπ₯ β π’ π) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π))) |
31 | 13, 30 | imbi12d 234 |
. . 3
β’ (π’ = (π€ βͺ {π§}) β ((βπ₯ β π’ βπ¦ β π΅ π β βπ(π:π’βΆπ΅ β§ βπ₯ β π’ π)) β (βπ₯ β (π€ βͺ {π§})βπ¦ β π΅ π β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)))) |
32 | | raleq 2672 |
. . . 4
β’ (π’ = π΄ β (βπ₯ β π’ βπ¦ β π΅ π β βπ₯ β π΄ βπ¦ β π΅ π)) |
33 | | feq2 5349 |
. . . . . 6
β’ (π’ = π΄ β (π:π’βΆπ΅ β π:π΄βΆπ΅)) |
34 | | raleq 2672 |
. . . . . 6
β’ (π’ = π΄ β (βπ₯ β π’ π β βπ₯ β π΄ π)) |
35 | 33, 34 | anbi12d 473 |
. . . . 5
β’ (π’ = π΄ β ((π:π’βΆπ΅ β§ βπ₯ β π’ π) β (π:π΄βΆπ΅ β§ βπ₯ β π΄ π))) |
36 | 35 | exbidv 1825 |
. . . 4
β’ (π’ = π΄ β (βπ(π:π’βΆπ΅ β§ βπ₯ β π’ π) β βπ(π:π΄βΆπ΅ β§ βπ₯ β π΄ π))) |
37 | 32, 36 | imbi12d 234 |
. . 3
β’ (π’ = π΄ β ((βπ₯ β π’ βπ¦ β π΅ π β βπ(π:π’βΆπ΅ β§ βπ₯ β π’ π)) β (βπ₯ β π΄ βπ¦ β π΅ π β βπ(π:π΄βΆπ΅ β§ βπ₯ β π΄ π)))) |
38 | | f0 5406 |
. . . 4
β’
β
:β
βΆπ΅ |
39 | | 0ex 4130 |
. . . . 5
β’ β
β V |
40 | | ral0 3524 |
. . . . . . 7
β’
βπ₯ β
β
π |
41 | 40 | biantru 302 |
. . . . . 6
β’ (π:β
βΆπ΅ β (π:β
βΆπ΅ β§ βπ₯ β β
π)) |
42 | | feq1 5348 |
. . . . . 6
β’ (π = β
β (π:β
βΆπ΅ β
β
:β
βΆπ΅)) |
43 | 41, 42 | bitr3id 194 |
. . . . 5
β’ (π = β
β ((π:β
βΆπ΅ β§ βπ₯ β β
π) β β
:β
βΆπ΅)) |
44 | 39, 43 | spcev 2832 |
. . . 4
β’
(β
:β
βΆπ΅ β βπ(π:β
βΆπ΅ β§ βπ₯ β β
π)) |
45 | 38, 44 | mp1i 10 |
. . 3
β’
(βπ₯ β
β
βπ¦ β
π΅ π β βπ(π:β
βΆπ΅ β§ βπ₯ β β
π)) |
46 | | ssun1 3298 |
. . . . . . 7
β’ π€ β (π€ βͺ {π§}) |
47 | | ssralv 3219 |
. . . . . . 7
β’ (π€ β (π€ βͺ {π§}) β (βπ₯ β (π€ βͺ {π§})βπ¦ β π΅ π β βπ₯ β π€ βπ¦ β π΅ π)) |
48 | 46, 47 | ax-mp 5 |
. . . . . 6
β’
(βπ₯ β
(π€ βͺ {π§})βπ¦ β π΅ π β βπ₯ β π€ βπ¦ β π΅ π) |
49 | 48 | imim1i 60 |
. . . . 5
β’
((βπ₯ β
π€ βπ¦ β π΅ π β βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π)) β (βπ₯ β (π€ βͺ {π§})βπ¦ β π΅ π β βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π))) |
50 | | ssun2 3299 |
. . . . . . . . 9
β’ {π§} β (π€ βͺ {π§}) |
51 | | ssralv 3219 |
. . . . . . . . 9
β’ ({π§} β (π€ βͺ {π§}) β (βπ₯ β (π€ βͺ {π§})βπ¦ β π΅ π β βπ₯ β {π§}βπ¦ β π΅ π)) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . 8
β’
(βπ₯ β
(π€ βͺ {π§})βπ¦ β π΅ π β βπ₯ β {π§}βπ¦ β π΅ π) |
53 | | vex 2740 |
. . . . . . . . . 10
β’ π§ β V |
54 | | ralsnsg 3629 |
. . . . . . . . . 10
β’ (π§ β V β (βπ₯ β {π§}βπ¦ β π΅ π β [π§ / π₯]βπ¦ β π΅ π)) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ₯ β
{π§}βπ¦ β π΅ π β [π§ / π₯]βπ¦ β π΅ π) |
56 | | sbcrex 3042 |
. . . . . . . . 9
β’
([π§ / π₯]βπ¦ β π΅ π β βπ¦ β π΅ [π§ / π₯]π) |
57 | 55, 56 | bitri 184 |
. . . . . . . 8
β’
(βπ₯ β
{π§}βπ¦ β π΅ π β βπ¦ β π΅ [π§ / π₯]π) |
58 | 52, 57 | sylib 122 |
. . . . . . 7
β’
(βπ₯ β
(π€ βͺ {π§})βπ¦ β π΅ π β βπ¦ β π΅ [π§ / π₯]π) |
59 | | nfv 1528 |
. . . . . . . 8
β’
β²π¦ Β¬ π§ β π€ |
60 | | nfv 1528 |
. . . . . . . . 9
β’
β²π¦βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π) |
61 | | nfv 1528 |
. . . . . . . . . . 11
β’
β²π¦ π:(π€ βͺ {π§})βΆπ΅ |
62 | | nfcv 2319 |
. . . . . . . . . . . 12
β’
β²π¦(π€ βͺ {π§}) |
63 | | nfsbc1v 2981 |
. . . . . . . . . . . 12
β’
β²π¦[(πβπ₯) / π¦]π |
64 | 62, 63 | nfralxy 2515 |
. . . . . . . . . . 11
β’
β²π¦βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π |
65 | 61, 64 | nfan 1565 |
. . . . . . . . . 10
β’
β²π¦(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π) |
66 | 65 | nfex 1637 |
. . . . . . . . 9
β’
β²π¦βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π) |
67 | 60, 66 | nfim 1572 |
. . . . . . . 8
β’
β²π¦(βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)) |
68 | | simprl 529 |
. . . . . . . . . . . . 13
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β π:π€βΆπ΅) |
69 | | vex 2740 |
. . . . . . . . . . . . . . . 16
β’ π¦ β V |
70 | 53, 69 | f1osn 5501 |
. . . . . . . . . . . . . . 15
β’
{β¨π§, π¦β©}:{π§}β1-1-ontoβ{π¦} |
71 | | f1of 5461 |
. . . . . . . . . . . . . . 15
β’
({β¨π§, π¦β©}:{π§}β1-1-ontoβ{π¦} β {β¨π§, π¦β©}:{π§}βΆ{π¦}) |
72 | 70, 71 | mp1i 10 |
. . . . . . . . . . . . . 14
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β {β¨π§, π¦β©}:{π§}βΆ{π¦}) |
73 | | simpl2 1001 |
. . . . . . . . . . . . . . 15
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β π¦ β π΅) |
74 | 73 | snssd 3737 |
. . . . . . . . . . . . . 14
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β {π¦} β π΅) |
75 | 72, 74 | fssd 5378 |
. . . . . . . . . . . . 13
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β {β¨π§, π¦β©}:{π§}βΆπ΅) |
76 | | simpl1 1000 |
. . . . . . . . . . . . . 14
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β Β¬ π§ β π€) |
77 | | disjsn 3654 |
. . . . . . . . . . . . . 14
β’ ((π€ β© {π§}) = β
β Β¬ π§ β π€) |
78 | 76, 77 | sylibr 134 |
. . . . . . . . . . . . 13
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β (π€ β© {π§}) = β
) |
79 | | fun2 5389 |
. . . . . . . . . . . . 13
β’ (((π:π€βΆπ΅ β§ {β¨π§, π¦β©}:{π§}βΆπ΅) β§ (π€ β© {π§}) = β
) β (π βͺ {β¨π§, π¦β©}):(π€ βͺ {π§})βΆπ΅) |
80 | 68, 75, 78, 79 | syl21anc 1237 |
. . . . . . . . . . . 12
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β (π βͺ {β¨π§, π¦β©}):(π€ βͺ {π§})βΆπ΅) |
81 | | simprr 531 |
. . . . . . . . . . . . . 14
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β βπ₯ β π€ π) |
82 | | eleq1a 2249 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π€ β (π§ = π₯ β π§ β π€)) |
83 | 82 | necon3bd 2390 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β π€ β (Β¬ π§ β π€ β π§ β π₯)) |
84 | 83 | impcom 125 |
. . . . . . . . . . . . . . . . 17
β’ ((Β¬
π§ β π€ β§ π₯ β π€) β π§ β π₯) |
85 | | fvunsng 5710 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β V β§ π§ β π₯) β ((π βͺ {β¨π§, π¦β©})βπ₯) = (πβπ₯)) |
86 | 20, 85 | mpan 424 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β π₯ β ((π βͺ {β¨π§, π¦β©})βπ₯) = (πβπ₯)) |
87 | | dfsbcq 2964 |
. . . . . . . . . . . . . . . . . 18
β’ (((π βͺ {β¨π§, π¦β©})βπ₯) = (πβπ₯) β ([((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π β [(πβπ₯) / π¦]π)) |
88 | 87, 23 | bitr2di 197 |
. . . . . . . . . . . . . . . . 17
β’ (((π βͺ {β¨π§, π¦β©})βπ₯) = (πβπ₯) β (π β [((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
89 | 84, 86, 88 | 3syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((Β¬
π§ β π€ β§ π₯ β π€) β (π β [((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
90 | 89 | ralbidva 2473 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π§ β π€ β (βπ₯ β π€ π β βπ₯ β π€ [((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
91 | 76, 90 | syl 14 |
. . . . . . . . . . . . . 14
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β (βπ₯ β π€ π β βπ₯ β π€ [((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
92 | 81, 91 | mpbid 147 |
. . . . . . . . . . . . 13
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β βπ₯ β π€ [((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π) |
93 | | simpl3 1002 |
. . . . . . . . . . . . . 14
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β [π§ / π₯]π) |
94 | | ffun 5368 |
. . . . . . . . . . . . . . . . 17
β’ ((π βͺ {β¨π§, π¦β©}):(π€ βͺ {π§})βΆπ΅ β Fun (π βͺ {β¨π§, π¦β©})) |
95 | | ssun2 3299 |
. . . . . . . . . . . . . . . . . 18
β’
{β¨π§, π¦β©} β (π βͺ {β¨π§, π¦β©}) |
96 | | vsnid 3624 |
. . . . . . . . . . . . . . . . . . 19
β’ π§ β {π§} |
97 | 69 | dmsnop 5102 |
. . . . . . . . . . . . . . . . . . 19
β’ dom
{β¨π§, π¦β©} = {π§} |
98 | 96, 97 | eleqtrri 2253 |
. . . . . . . . . . . . . . . . . 18
β’ π§ β dom {β¨π§, π¦β©} |
99 | | funssfv 5541 |
. . . . . . . . . . . . . . . . . 18
β’ ((Fun
(π βͺ {β¨π§, π¦β©}) β§ {β¨π§, π¦β©} β (π βͺ {β¨π§, π¦β©}) β§ π§ β dom {β¨π§, π¦β©}) β ((π βͺ {β¨π§, π¦β©})βπ§) = ({β¨π§, π¦β©}βπ§)) |
100 | 95, 98, 99 | mp3an23 1329 |
. . . . . . . . . . . . . . . . 17
β’ (Fun
(π βͺ {β¨π§, π¦β©}) β ((π βͺ {β¨π§, π¦β©})βπ§) = ({β¨π§, π¦β©}βπ§)) |
101 | 80, 94, 100 | 3syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β ((π βͺ {β¨π§, π¦β©})βπ§) = ({β¨π§, π¦β©}βπ§)) |
102 | 53, 69 | fvsn 5711 |
. . . . . . . . . . . . . . . 16
β’
({β¨π§, π¦β©}βπ§) = π¦ |
103 | 101, 102 | eqtr2di 2227 |
. . . . . . . . . . . . . . 15
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β π¦ = ((π βͺ {β¨π§, π¦β©})βπ§)) |
104 | | ralsnsg 3629 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β V β (βπ₯ β {π§}π β [π§ / π₯]π)) |
105 | 53, 104 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(βπ₯ β
{π§}π β [π§ / π₯]π) |
106 | | elsni 3610 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β {π§} β π₯ = π§) |
107 | 106 | fveq2d 5519 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β {π§} β ((π βͺ {β¨π§, π¦β©})βπ₯) = ((π βͺ {β¨π§, π¦β©})βπ§)) |
108 | 107 | eqeq2d 2189 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β {π§} β (π¦ = ((π βͺ {β¨π§, π¦β©})βπ₯) β π¦ = ((π βͺ {β¨π§, π¦β©})βπ§))) |
109 | 108 | biimparc 299 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ = ((π βͺ {β¨π§, π¦β©})βπ§) β§ π₯ β {π§}) β π¦ = ((π βͺ {β¨π§, π¦β©})βπ₯)) |
110 | | sbceq1a 2972 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = ((π βͺ {β¨π§, π¦β©})βπ₯) β (π β [((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
111 | 109, 110 | syl 14 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ = ((π βͺ {β¨π§, π¦β©})βπ§) β§ π₯ β {π§}) β (π β [((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
112 | 111 | ralbidva 2473 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = ((π βͺ {β¨π§, π¦β©})βπ§) β (βπ₯ β {π§}π β βπ₯ β {π§}[((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
113 | 105, 112 | bitr3id 194 |
. . . . . . . . . . . . . . 15
β’ (π¦ = ((π βͺ {β¨π§, π¦β©})βπ§) β ([π§ / π₯]π β βπ₯ β {π§}[((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
114 | 103, 113 | syl 14 |
. . . . . . . . . . . . . 14
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β ([π§ / π₯]π β βπ₯ β {π§}[((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
115 | 93, 114 | mpbid 147 |
. . . . . . . . . . . . 13
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β βπ₯ β {π§}[((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π) |
116 | | ralun 3317 |
. . . . . . . . . . . . 13
β’
((βπ₯ β
π€ [((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π β§ βπ₯ β {π§}[((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π) β βπ₯ β (π€ βͺ {π§})[((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π) |
117 | 92, 115, 116 | syl2anc 411 |
. . . . . . . . . . . 12
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β βπ₯ β (π€ βͺ {π§})[((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π) |
118 | 53, 69 | opex 4229 |
. . . . . . . . . . . . . . 15
β’
β¨π§, π¦β© β V |
119 | 118 | snex 4185 |
. . . . . . . . . . . . . 14
β’
{β¨π§, π¦β©} β
V |
120 | 19, 119 | unex 4441 |
. . . . . . . . . . . . 13
β’ (π βͺ {β¨π§, π¦β©}) β V |
121 | | feq1 5348 |
. . . . . . . . . . . . . 14
β’ (π = (π βͺ {β¨π§, π¦β©}) β (π:(π€ βͺ {π§})βΆπ΅ β (π βͺ {β¨π§, π¦β©}):(π€ βͺ {π§})βΆπ΅)) |
122 | | fveq1 5514 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βͺ {β¨π§, π¦β©}) β (πβπ₯) = ((π βͺ {β¨π§, π¦β©})βπ₯)) |
123 | 122 | sbceq1d 2967 |
. . . . . . . . . . . . . . 15
β’ (π = (π βͺ {β¨π§, π¦β©}) β ([(πβπ₯) / π¦]π β [((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
124 | 123 | ralbidv 2477 |
. . . . . . . . . . . . . 14
β’ (π = (π βͺ {β¨π§, π¦β©}) β (βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π β βπ₯ β (π€ βͺ {π§})[((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π)) |
125 | 121, 124 | anbi12d 473 |
. . . . . . . . . . . . 13
β’ (π = (π βͺ {β¨π§, π¦β©}) β ((π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π) β ((π βͺ {β¨π§, π¦β©}):(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π))) |
126 | 120, 125 | spcev 2832 |
. . . . . . . . . . . 12
β’ (((π βͺ {β¨π§, π¦β©}):(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[((π βͺ {β¨π§, π¦β©})βπ₯) / π¦]π) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)) |
127 | 80, 117, 126 | syl2anc 411 |
. . . . . . . . . . 11
β’ (((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β§ (π:π€βΆπ΅ β§ βπ₯ β π€ π)) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)) |
128 | 127 | ex 115 |
. . . . . . . . . 10
β’ ((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β ((π:π€βΆπ΅ β§ βπ₯ β π€ π) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π))) |
129 | 128 | exlimdv 1819 |
. . . . . . . . 9
β’ ((Β¬
π§ β π€ β§ π¦ β π΅ β§ [π§ / π₯]π) β (βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π))) |
130 | 129 | 3exp 1202 |
. . . . . . . 8
β’ (Β¬
π§ β π€ β (π¦ β π΅ β ([π§ / π₯]π β (βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π))))) |
131 | 59, 67, 130 | rexlimd 2591 |
. . . . . . 7
β’ (Β¬
π§ β π€ β (βπ¦ β π΅ [π§ / π₯]π β (βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)))) |
132 | 58, 131 | syl5 32 |
. . . . . 6
β’ (Β¬
π§ β π€ β (βπ₯ β (π€ βͺ {π§})βπ¦ β π΅ π β (βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π) β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)))) |
133 | 132 | a2d 26 |
. . . . 5
β’ (Β¬
π§ β π€ β ((βπ₯ β (π€ βͺ {π§})βπ¦ β π΅ π β βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π)) β (βπ₯ β (π€ βͺ {π§})βπ¦ β π΅ π β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)))) |
134 | 49, 133 | syl5 32 |
. . . 4
β’ (Β¬
π§ β π€ β ((βπ₯ β π€ βπ¦ β π΅ π β βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π)) β (βπ₯ β (π€ βͺ {π§})βπ¦ β π΅ π β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)))) |
135 | 134 | adantl 277 |
. . 3
β’ ((π€ β Fin β§ Β¬ π§ β π€) β ((βπ₯ β π€ βπ¦ β π΅ π β βπ(π:π€βΆπ΅ β§ βπ₯ β π€ π)) β (βπ₯ β (π€ βͺ {π§})βπ¦ β π΅ π β βπ(π:(π€ βͺ {π§})βΆπ΅ β§ βπ₯ β (π€ βͺ {π§})[(πβπ₯) / π¦]π)))) |
136 | 6, 12, 31, 37, 45, 135 | findcard2s 6889 |
. 2
β’ (π΄ β Fin β
(βπ₯ β π΄ βπ¦ β π΅ π β βπ(π:π΄βΆπ΅ β§ βπ₯ β π΄ π))) |
137 | 136 | imp 124 |
1
β’ ((π΄ β Fin β§ βπ₯ β π΄ βπ¦ β π΅ π) β βπ(π:π΄βΆπ΅ β§ βπ₯ β π΄ π)) |