Step | Hyp | Ref
| Expression |
1 | | wessf1ornlem.a |
. . . 4
β’ (π β π΄ β π) |
2 | | cnvimass 6081 |
. . . . . . . 8
β’ (β‘πΉ β {π’}) β dom πΉ |
3 | | wessf1ornlem.f |
. . . . . . . . . 10
β’ (π β πΉ Fn π΄) |
4 | 3 | fndmd 6655 |
. . . . . . . . 9
β’ (π β dom πΉ = π΄) |
5 | 4 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π’ β ran πΉ) β dom πΉ = π΄) |
6 | 2, 5 | sseqtrid 4035 |
. . . . . . 7
β’ ((π β§ π’ β ran πΉ) β (β‘πΉ β {π’}) β π΄) |
7 | | wessf1ornlem.r |
. . . . . . . . . 10
β’ (π β π
We π΄) |
8 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π’ β ran πΉ) β π
We π΄) |
9 | 2, 4 | sseqtrid 4035 |
. . . . . . . . . . 11
β’ (π β (β‘πΉ β {π’}) β π΄) |
10 | 1, 9 | ssexd 5325 |
. . . . . . . . . 10
β’ (π β (β‘πΉ β {π’}) β V) |
11 | 10 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π’ β ran πΉ) β (β‘πΉ β {π’}) β V) |
12 | | inisegn0 6098 |
. . . . . . . . . . 11
β’ (π’ β ran πΉ β (β‘πΉ β {π’}) β β
) |
13 | 12 | biimpi 215 |
. . . . . . . . . 10
β’ (π’ β ran πΉ β (β‘πΉ β {π’}) β β
) |
14 | 13 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π’ β ran πΉ) β (β‘πΉ β {π’}) β β
) |
15 | | wereu 5673 |
. . . . . . . . 9
β’ ((π
We π΄ β§ ((β‘πΉ β {π’}) β V β§ (β‘πΉ β {π’}) β π΄ β§ (β‘πΉ β {π’}) β β
)) β β!π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) |
16 | 8, 11, 6, 14, 15 | syl13anc 1373 |
. . . . . . . 8
β’ ((π β§ π’ β ran πΉ) β β!π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) |
17 | | riotacl 7383 |
. . . . . . . 8
β’
(β!π£ β
(β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£ β (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β (β‘πΉ β {π’})) |
18 | 16, 17 | syl 17 |
. . . . . . 7
β’ ((π β§ π’ β ran πΉ) β (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β (β‘πΉ β {π’})) |
19 | 6, 18 | sseldd 3984 |
. . . . . 6
β’ ((π β§ π’ β ran πΉ) β (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β π΄) |
20 | 19 | ralrimiva 3147 |
. . . . 5
β’ (π β βπ’ β ran πΉ(β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β π΄) |
21 | | wessf1ornlem.g |
. . . . . . 7
β’ πΊ = (π¦ β ran πΉ β¦ (β©π₯ β (β‘πΉ β {π¦})βπ§ β (β‘πΉ β {π¦}) Β¬ π§π
π₯)) |
22 | | sneq 4639 |
. . . . . . . . . . 11
β’ (π¦ = π’ β {π¦} = {π’}) |
23 | 22 | imaeq2d 6060 |
. . . . . . . . . 10
β’ (π¦ = π’ β (β‘πΉ β {π¦}) = (β‘πΉ β {π’})) |
24 | 23 | raleqdv 3326 |
. . . . . . . . . 10
β’ (π¦ = π’ β (βπ§ β (β‘πΉ β {π¦}) Β¬ π§π
π₯ β βπ§ β (β‘πΉ β {π’}) Β¬ π§π
π₯)) |
25 | 23, 24 | riotaeqbidv 7368 |
. . . . . . . . 9
β’ (π¦ = π’ β (β©π₯ β (β‘πΉ β {π¦})βπ§ β (β‘πΉ β {π¦}) Β¬ π§π
π₯) = (β©π₯ β (β‘πΉ β {π’})βπ§ β (β‘πΉ β {π’}) Β¬ π§π
π₯)) |
26 | | breq1 5152 |
. . . . . . . . . . . . 13
β’ (π§ = π‘ β (π§π
π₯ β π‘π
π₯)) |
27 | 26 | notbid 318 |
. . . . . . . . . . . 12
β’ (π§ = π‘ β (Β¬ π§π
π₯ β Β¬ π‘π
π₯)) |
28 | 27 | cbvralvw 3235 |
. . . . . . . . . . 11
β’
(βπ§ β
(β‘πΉ β {π’}) Β¬ π§π
π₯ β βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π₯) |
29 | | breq2 5153 |
. . . . . . . . . . . . 13
β’ (π₯ = π£ β (π‘π
π₯ β π‘π
π£)) |
30 | 29 | notbid 318 |
. . . . . . . . . . . 12
β’ (π₯ = π£ β (Β¬ π‘π
π₯ β Β¬ π‘π
π£)) |
31 | 30 | ralbidv 3178 |
. . . . . . . . . . 11
β’ (π₯ = π£ β (βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π₯ β βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
32 | 28, 31 | bitrid 283 |
. . . . . . . . . 10
β’ (π₯ = π£ β (βπ§ β (β‘πΉ β {π’}) Β¬ π§π
π₯ β βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
33 | 32 | cbvriotavw 7375 |
. . . . . . . . 9
β’
(β©π₯
β (β‘πΉ β {π’})βπ§ β (β‘πΉ β {π’}) Β¬ π§π
π₯) = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) |
34 | 25, 33 | eqtrdi 2789 |
. . . . . . . 8
β’ (π¦ = π’ β (β©π₯ β (β‘πΉ β {π¦})βπ§ β (β‘πΉ β {π¦}) Β¬ π§π
π₯) = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
35 | 34 | cbvmptv 5262 |
. . . . . . 7
β’ (π¦ β ran πΉ β¦ (β©π₯ β (β‘πΉ β {π¦})βπ§ β (β‘πΉ β {π¦}) Β¬ π§π
π₯)) = (π’ β ran πΉ β¦ (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
36 | 21, 35 | eqtri 2761 |
. . . . . 6
β’ πΊ = (π’ β ran πΉ β¦ (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
37 | 36 | rnmptss 7122 |
. . . . 5
β’
(βπ’ β
ran πΉ(β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β π΄ β ran πΊ β π΄) |
38 | 20, 37 | syl 17 |
. . . 4
β’ (π β ran πΊ β π΄) |
39 | 1, 38 | sselpwd 5327 |
. . 3
β’ (π β ran πΊ β π« π΄) |
40 | | dffn3 6731 |
. . . . . . 7
β’ (πΉ Fn π΄ β πΉ:π΄βΆran πΉ) |
41 | 3, 40 | sylib 217 |
. . . . . 6
β’ (π β πΉ:π΄βΆran πΉ) |
42 | 41, 38 | fssresd 6759 |
. . . . 5
β’ (π β (πΉ βΎ ran πΊ):ran πΊβΆran πΉ) |
43 | | fvres 6911 |
. . . . . . . . . . . . 13
β’ (π€ β ran πΊ β ((πΉ βΎ ran πΊ)βπ€) = (πΉβπ€)) |
44 | 43 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (π€ β ran πΊ β (πΉβπ€) = ((πΉ βΎ ran πΊ)βπ€)) |
45 | 44 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π€ β ran πΊ β§ π‘ β ran πΊ) β§ ((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘)) β (πΉβπ€) = ((πΉ βΎ ran πΊ)βπ€)) |
46 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π€ β ran πΊ β§ π‘ β ran πΊ) β§ ((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘)) β ((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘)) |
47 | | fvres 6911 |
. . . . . . . . . . . 12
β’ (π‘ β ran πΊ β ((πΉ βΎ ran πΊ)βπ‘) = (πΉβπ‘)) |
48 | 47 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π€ β ran πΊ β§ π‘ β ran πΊ) β§ ((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘)) β ((πΉ βΎ ran πΊ)βπ‘) = (πΉβπ‘)) |
49 | 45, 46, 48 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (((π€ β ran πΊ β§ π‘ β ran πΊ) β§ ((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘)) β (πΉβπ€) = (πΉβπ‘)) |
50 | 49 | 3adantl1 1167 |
. . . . . . . . 9
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ ((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘)) β (πΉβπ€) = (πΉβπ‘)) |
51 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β π) |
52 | | simpl3 1194 |
. . . . . . . . . . 11
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β π‘ β ran πΊ) |
53 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β π€ β ran πΊ) |
54 | | id 22 |
. . . . . . . . . . . . 13
β’ ((πΉβπ€) = (πΉβπ‘) β (πΉβπ€) = (πΉβπ‘)) |
55 | 54 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((πΉβπ€) = (πΉβπ‘) β (πΉβπ‘) = (πΉβπ€)) |
56 | 55 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β (πΉβπ‘) = (πΉβπ€)) |
57 | | eleq1w 2817 |
. . . . . . . . . . . . . . 15
β’ (π = π€ β (π β ran πΊ β π€ β ran πΊ)) |
58 | 57 | 3anbi3d 1443 |
. . . . . . . . . . . . . 14
β’ (π = π€ β ((π β§ π‘ β ran πΊ β§ π β ran πΊ) β (π β§ π‘ β ran πΊ β§ π€ β ran πΊ))) |
59 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π = π€ β (πΉβπ) = (πΉβπ€)) |
60 | 59 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
β’ (π = π€ β ((πΉβπ‘) = (πΉβπ) β (πΉβπ‘) = (πΉβπ€))) |
61 | 58, 60 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π = π€ β (((π β§ π‘ β ran πΊ β§ π β ran πΊ) β§ (πΉβπ‘) = (πΉβπ)) β ((π β§ π‘ β ran πΊ β§ π€ β ran πΊ) β§ (πΉβπ‘) = (πΉβπ€)))) |
62 | | breq1 5152 |
. . . . . . . . . . . . . 14
β’ (π = π€ β (ππ
π‘ β π€π
π‘)) |
63 | 62 | notbid 318 |
. . . . . . . . . . . . 13
β’ (π = π€ β (Β¬ ππ
π‘ β Β¬ π€π
π‘)) |
64 | 61, 63 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = π€ β ((((π β§ π‘ β ran πΊ β§ π β ran πΊ) β§ (πΉβπ‘) = (πΉβπ)) β Β¬ ππ
π‘) β (((π β§ π‘ β ran πΊ β§ π€ β ran πΊ) β§ (πΉβπ‘) = (πΉβπ€)) β Β¬ π€π
π‘))) |
65 | | eleq1w 2817 |
. . . . . . . . . . . . . . . 16
β’ (π = π‘ β (π β ran πΊ β π‘ β ran πΊ)) |
66 | 65 | 3anbi2d 1442 |
. . . . . . . . . . . . . . 15
β’ (π = π‘ β ((π β§ π β ran πΊ β§ π β ran πΊ) β (π β§ π‘ β ran πΊ β§ π β ran πΊ))) |
67 | | fveqeq2 6901 |
. . . . . . . . . . . . . . 15
β’ (π = π‘ β ((πΉβπ) = (πΉβπ) β (πΉβπ‘) = (πΉβπ))) |
68 | 66, 67 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π = π‘ β (((π β§ π β ran πΊ β§ π β ran πΊ) β§ (πΉβπ) = (πΉβπ)) β ((π β§ π‘ β ran πΊ β§ π β ran πΊ) β§ (πΉβπ‘) = (πΉβπ)))) |
69 | | breq2 5153 |
. . . . . . . . . . . . . . 15
β’ (π = π‘ β (ππ
π β ππ
π‘)) |
70 | 69 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (π = π‘ β (Β¬ ππ
π β Β¬ ππ
π‘)) |
71 | 68, 70 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = π‘ β ((((π β§ π β ran πΊ β§ π β ran πΊ) β§ (πΉβπ) = (πΉβπ)) β Β¬ ππ
π) β (((π β§ π‘ β ran πΊ β§ π β ran πΊ) β§ (πΉβπ‘) = (πΉβπ)) β Β¬ ππ
π‘))) |
72 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = π β (π‘ β ran πΊ β π β ran πΊ)) |
73 | 72 | 3anbi3d 1443 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = π β ((π β§ π β ran πΊ β§ π‘ β ran πΊ) β (π β§ π β ran πΊ β§ π β ran πΊ))) |
74 | | fveq2 6892 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = π β (πΉβπ‘) = (πΉβπ)) |
75 | 74 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = π β ((πΉβπ) = (πΉβπ‘) β (πΉβπ) = (πΉβπ))) |
76 | 73, 75 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π‘ = π β (((π β§ π β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ) = (πΉβπ‘)) β ((π β§ π β ran πΊ β§ π β ran πΊ) β§ (πΉβπ) = (πΉβπ)))) |
77 | | breq1 5152 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = π β (π‘π
π β ππ
π)) |
78 | 77 | notbid 318 |
. . . . . . . . . . . . . . 15
β’ (π‘ = π β (Β¬ π‘π
π β Β¬ ππ
π)) |
79 | 76, 78 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β ((((π β§ π β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ) = (πΉβπ‘)) β Β¬ π‘π
π) β (((π β§ π β ran πΊ β§ π β ran πΊ) β§ (πΉβπ) = (πΉβπ)) β Β¬ ππ
π))) |
80 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = π β (π€ β ran πΊ β π β ran πΊ)) |
81 | 80 | 3anbi2d 1442 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π β ((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β (π β§ π β ran πΊ β§ π‘ β ran πΊ))) |
82 | | fveqeq2 6901 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π β ((πΉβπ€) = (πΉβπ‘) β (πΉβπ) = (πΉβπ‘))) |
83 | 81, 82 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π β (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β ((π β§ π β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ) = (πΉβπ‘)))) |
84 | | breq2 5153 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π β (π‘π
π€ β π‘π
π)) |
85 | 84 | notbid 318 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π β (Β¬ π‘π
π€ β Β¬ π‘π
π)) |
86 | 83, 85 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π€ = π β ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β Β¬ π‘π
π€) β (((π β§ π β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ) = (πΉβπ‘)) β Β¬ π‘π
π))) |
87 | 36 | elrnmpt 5956 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β V β (π€ β ran πΊ β βπ’ β ran πΉ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£))) |
88 | 87 | elv 3481 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ β ran πΊ β βπ’ β ran πΉ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
89 | 88 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β ran πΊ β βπ’ β ran πΉ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
90 | 89 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π€ β ran πΊ β§ (πΉβπ€) = (πΉβπ‘)) β βπ’ β ran πΉ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
91 | 90 | 3ad2antl2 1187 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β βπ’ β ran πΉ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
92 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
93 | 92 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) = π€) |
94 | | simp11 1204 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β π) |
95 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
96 | | breq2 5153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π£ = π€ β (π‘π
π£ β π‘π
π€)) |
97 | 96 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π£ = π€ β (Β¬ π‘π
π£ β Β¬ π‘π
π€)) |
98 | 97 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π£ = π€ β (βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£ β βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€)) |
99 | 98 | cbvriotavw 7375 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(β©π£
β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) = (β©π€ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) |
100 | 95, 99 | eqtr2di 2790 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β (β©π€ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) = π€) |
101 | 100 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (β©π€ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) = π€) |
102 | 98 | cbvreuvw 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(β!π£ β
(β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£ β β!π€ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) |
103 | 16, 102 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π’ β ran πΉ) β β!π€ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) |
104 | | riota1 7387 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(β!π€ β
(β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€ β ((π€ β (β‘πΉ β {π’}) β§ βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) β (β©π€ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) = π€)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π’ β ran πΉ) β ((π€ β (β‘πΉ β {π’}) β§ βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) β (β©π€ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) = π€)) |
106 | 105 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β ((π€ β (β‘πΉ β {π’}) β§ βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) β (β©π€ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) = π€)) |
107 | 101, 106 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (π€ β (β‘πΉ β {π’}) β§ βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€)) |
108 | 107 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β π€ β (β‘πΉ β {π’})) |
109 | 94, 108 | syld3an1 1411 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β π€ β (β‘πΉ β {π’})) |
110 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β π’ β ran πΉ) |
111 | 94, 110, 16 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β β!π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) |
112 | 98 | riota2 7391 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π€ β (β‘πΉ β {π’}) β§ β!π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β (βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€ β (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) = π€)) |
113 | 109, 111,
112 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€ β (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) = π€)) |
114 | 93, 113 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) |
115 | 114 | 3adant1r 1178 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π€) |
116 | 38 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π‘ β ran πΊ) β π‘ β π΄) |
117 | 116 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β π‘ β π΄) |
118 | 117 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β π‘ β π΄) |
119 | 118 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β π‘ β π΄) |
120 | 55 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β§ π’ β ran πΉ) β (πΉβπ‘) = (πΉβπ€)) |
121 | 120 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (πΉβπ‘) = (πΉβπ€)) |
122 | | fniniseg 7062 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πΉ Fn π΄ β (π€ β (β‘πΉ β {π’}) β (π€ β π΄ β§ (πΉβπ€) = π’))) |
123 | 94, 3, 122 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (π€ β (β‘πΉ β {π’}) β (π€ β π΄ β§ (πΉβπ€) = π’))) |
124 | 109, 123 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (π€ β π΄ β§ (πΉβπ€) = π’)) |
125 | 124 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (πΉβπ€) = π’) |
126 | 125 | 3adant1r 1178 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (πΉβπ€) = π’) |
127 | 121, 126 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (πΉβπ‘) = π’) |
128 | | fniniseg 7062 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΉ Fn π΄ β (π‘ β (β‘πΉ β {π’}) β (π‘ β π΄ β§ (πΉβπ‘) = π’))) |
129 | 3, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π‘ β (β‘πΉ β {π’}) β (π‘ β π΄ β§ (πΉβπ‘) = π’))) |
130 | 129 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β (π‘ β (β‘πΉ β {π’}) β (π‘ β π΄ β§ (πΉβπ‘) = π’))) |
131 | 130 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β§ π’ β ran πΉ) β (π‘ β (β‘πΉ β {π’}) β (π‘ β π΄ β§ (πΉβπ‘) = π’))) |
132 | 131 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β (π‘ β (β‘πΉ β {π’}) β (π‘ β π΄ β§ (πΉβπ‘) = π’))) |
133 | 119, 127,
132 | mpbir2and 712 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β π‘ β (β‘πΉ β {π’})) |
134 | | rspa 3246 |
. . . . . . . . . . . . . . . . . 18
β’
((βπ‘ β
(β‘πΉ β {π’}) Β¬ π‘π
π€ β§ π‘ β (β‘πΉ β {π’})) β Β¬ π‘π
π€) |
135 | 115, 133,
134 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β§ π’ β ran πΉ β§ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) β Β¬ π‘π
π€) |
136 | 135 | rexlimdv3a 3160 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β (βπ’ β ran πΉ π€ = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β Β¬ π‘π
π€)) |
137 | 91, 136 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β Β¬ π‘π
π€) |
138 | 86, 137 | chvarvv 2003 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ) = (πΉβπ‘)) β Β¬ π‘π
π) |
139 | 79, 138 | chvarvv 2003 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ran πΊ β§ π β ran πΊ) β§ (πΉβπ) = (πΉβπ)) β Β¬ ππ
π) |
140 | 71, 139 | chvarvv 2003 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β ran πΊ β§ π β ran πΊ) β§ (πΉβπ‘) = (πΉβπ)) β Β¬ ππ
π‘) |
141 | 64, 140 | chvarvv 2003 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β ran πΊ β§ π€ β ran πΊ) β§ (πΉβπ‘) = (πΉβπ€)) β Β¬ π€π
π‘) |
142 | 51, 52, 53, 56, 141 | syl31anc 1374 |
. . . . . . . . . 10
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β Β¬ π€π
π‘) |
143 | | weso 5668 |
. . . . . . . . . . . . . 14
β’ (π
We π΄ β π
Or π΄) |
144 | 7, 143 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π
Or π΄) |
145 | 144 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (πΉβπ€) = (πΉβπ‘)) β π
Or π΄) |
146 | 145 | 3ad2antl1 1186 |
. . . . . . . . . . 11
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β π
Or π΄) |
147 | 38 | sselda 3983 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β ran πΊ) β π€ β π΄) |
148 | 147 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β π€ β π΄) |
149 | 148 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β π€ β π΄) |
150 | | sotrieq2 5619 |
. . . . . . . . . . 11
β’ ((π
Or π΄ β§ (π€ β π΄ β§ π‘ β π΄)) β (π€ = π‘ β (Β¬ π€π
π‘ β§ Β¬ π‘π
π€))) |
151 | 146, 149,
118, 150 | syl12anc 836 |
. . . . . . . . . 10
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β (π€ = π‘ β (Β¬ π€π
π‘ β§ Β¬ π‘π
π€))) |
152 | 142, 137,
151 | mpbir2and 712 |
. . . . . . . . 9
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ (πΉβπ€) = (πΉβπ‘)) β π€ = π‘) |
153 | 50, 152 | syldan 592 |
. . . . . . . 8
β’ (((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β§ ((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘)) β π€ = π‘) |
154 | 153 | ex 414 |
. . . . . . 7
β’ ((π β§ π€ β ran πΊ β§ π‘ β ran πΊ) β (((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘) β π€ = π‘)) |
155 | 154 | 3expb 1121 |
. . . . . 6
β’ ((π β§ (π€ β ran πΊ β§ π‘ β ran πΊ)) β (((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘) β π€ = π‘)) |
156 | 155 | ralrimivva 3201 |
. . . . 5
β’ (π β βπ€ β ran πΊβπ‘ β ran πΊ(((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘) β π€ = π‘)) |
157 | | dff13 7254 |
. . . . 5
β’ ((πΉ βΎ ran πΊ):ran πΊβ1-1βran πΉ β ((πΉ βΎ ran πΊ):ran πΊβΆran πΉ β§ βπ€ β ran πΊβπ‘ β ran πΊ(((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)βπ‘) β π€ = π‘))) |
158 | 42, 156, 157 | sylanbrc 584 |
. . . 4
β’ (π β (πΉ βΎ ran πΊ):ran πΊβ1-1βran πΉ) |
159 | | riotaex 7369 |
. . . . . . . . . . 11
β’
(β©π£
β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β V |
160 | 159 | rgenw 3066 |
. . . . . . . . . 10
β’
βπ’ β ran
πΉ(β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β V |
161 | 36 | fnmpt 6691 |
. . . . . . . . . 10
β’
(βπ’ β
ran πΉ(β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β V β πΊ Fn ran πΉ) |
162 | 160, 161 | mp1i 13 |
. . . . . . . . 9
β’ (π β πΊ Fn ran πΉ) |
163 | | dffn3 6731 |
. . . . . . . . 9
β’ (πΊ Fn ran πΉ β πΊ:ran πΉβΆran πΊ) |
164 | 162, 163 | sylib 217 |
. . . . . . . 8
β’ (π β πΊ:ran πΉβΆran πΊ) |
165 | 164 | ffvelcdmda 7087 |
. . . . . . 7
β’ ((π β§ π’ β ran πΉ) β (πΊβπ’) β ran πΊ) |
166 | 165 | fvresd 6912 |
. . . . . . . 8
β’ ((π β§ π’ β ran πΉ) β ((πΉ βΎ ran πΊ)β(πΊβπ’)) = (πΉβ(πΊβπ’))) |
167 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β ran πΉ) β π’ β ran πΉ) |
168 | 159 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β ran πΉ) β (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£) β V) |
169 | 21, 34, 167, 168 | fvmptd3 7022 |
. . . . . . . . . . 11
β’ ((π β§ π’ β ran πΉ) β (πΊβπ’) = (β©π£ β (β‘πΉ β {π’})βπ‘ β (β‘πΉ β {π’}) Β¬ π‘π
π£)) |
170 | 169, 18 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π β§ π’ β ran πΉ) β (πΊβπ’) β (β‘πΉ β {π’})) |
171 | | fvex 6905 |
. . . . . . . . . . . 12
β’ (πΊβπ’) β V |
172 | | eleq1 2822 |
. . . . . . . . . . . . . 14
β’ (π€ = (πΊβπ’) β (π€ β (β‘πΉ β {π’}) β (πΊβπ’) β (β‘πΉ β {π’}))) |
173 | | eleq1 2822 |
. . . . . . . . . . . . . . 15
β’ (π€ = (πΊβπ’) β (π€ β π΄ β (πΊβπ’) β π΄)) |
174 | | fveqeq2 6901 |
. . . . . . . . . . . . . . 15
β’ (π€ = (πΊβπ’) β ((πΉβπ€) = π’ β (πΉβ(πΊβπ’)) = π’)) |
175 | 173, 174 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π€ = (πΊβπ’) β ((π€ β π΄ β§ (πΉβπ€) = π’) β ((πΊβπ’) β π΄ β§ (πΉβ(πΊβπ’)) = π’))) |
176 | 172, 175 | bibi12d 346 |
. . . . . . . . . . . . 13
β’ (π€ = (πΊβπ’) β ((π€ β (β‘πΉ β {π’}) β (π€ β π΄ β§ (πΉβπ€) = π’)) β ((πΊβπ’) β (β‘πΉ β {π’}) β ((πΊβπ’) β π΄ β§ (πΉβ(πΊβπ’)) = π’)))) |
177 | 176 | imbi2d 341 |
. . . . . . . . . . . 12
β’ (π€ = (πΊβπ’) β ((π β (π€ β (β‘πΉ β {π’}) β (π€ β π΄ β§ (πΉβπ€) = π’))) β (π β ((πΊβπ’) β (β‘πΉ β {π’}) β ((πΊβπ’) β π΄ β§ (πΉβ(πΊβπ’)) = π’))))) |
178 | 3, 122 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π€ β (β‘πΉ β {π’}) β (π€ β π΄ β§ (πΉβπ€) = π’))) |
179 | 171, 177,
178 | vtocl 3550 |
. . . . . . . . . . 11
β’ (π β ((πΊβπ’) β (β‘πΉ β {π’}) β ((πΊβπ’) β π΄ β§ (πΉβ(πΊβπ’)) = π’))) |
180 | 179 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π’ β ran πΉ) β ((πΊβπ’) β (β‘πΉ β {π’}) β ((πΊβπ’) β π΄ β§ (πΉβ(πΊβπ’)) = π’))) |
181 | 170, 180 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π’ β ran πΉ) β ((πΊβπ’) β π΄ β§ (πΉβ(πΊβπ’)) = π’)) |
182 | 181 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π’ β ran πΉ) β (πΉβ(πΊβπ’)) = π’) |
183 | 166, 182 | eqtr2d 2774 |
. . . . . . 7
β’ ((π β§ π’ β ran πΉ) β π’ = ((πΉ βΎ ran πΊ)β(πΊβπ’))) |
184 | | fveq2 6892 |
. . . . . . . 8
β’ (π€ = (πΊβπ’) β ((πΉ βΎ ran πΊ)βπ€) = ((πΉ βΎ ran πΊ)β(πΊβπ’))) |
185 | 184 | rspceeqv 3634 |
. . . . . . 7
β’ (((πΊβπ’) β ran πΊ β§ π’ = ((πΉ βΎ ran πΊ)β(πΊβπ’))) β βπ€ β ran πΊ π’ = ((πΉ βΎ ran πΊ)βπ€)) |
186 | 165, 183,
185 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π’ β ran πΉ) β βπ€ β ran πΊ π’ = ((πΉ βΎ ran πΊ)βπ€)) |
187 | 186 | ralrimiva 3147 |
. . . . 5
β’ (π β βπ’ β ran πΉβπ€ β ran πΊ π’ = ((πΉ βΎ ran πΊ)βπ€)) |
188 | | dffo3 7104 |
. . . . 5
β’ ((πΉ βΎ ran πΊ):ran πΊβontoβran πΉ β ((πΉ βΎ ran πΊ):ran πΊβΆran πΉ β§ βπ’ β ran πΉβπ€ β ran πΊ π’ = ((πΉ βΎ ran πΊ)βπ€))) |
189 | 42, 187, 188 | sylanbrc 584 |
. . . 4
β’ (π β (πΉ βΎ ran πΊ):ran πΊβontoβran πΉ) |
190 | | df-f1o 6551 |
. . . 4
β’ ((πΉ βΎ ran πΊ):ran πΊβ1-1-ontoβran
πΉ β ((πΉ βΎ ran πΊ):ran πΊβ1-1βran πΉ β§ (πΉ βΎ ran πΊ):ran πΊβontoβran πΉ)) |
191 | 158, 189,
190 | sylanbrc 584 |
. . 3
β’ (π β (πΉ βΎ ran πΊ):ran πΊβ1-1-ontoβran
πΉ) |
192 | | reseq2 5977 |
. . . . 5
β’ (π£ = ran πΊ β (πΉ βΎ π£) = (πΉ βΎ ran πΊ)) |
193 | | id 22 |
. . . . 5
β’ (π£ = ran πΊ β π£ = ran πΊ) |
194 | | eqidd 2734 |
. . . . 5
β’ (π£ = ran πΊ β ran πΉ = ran πΉ) |
195 | 192, 193,
194 | f1oeq123d 6828 |
. . . 4
β’ (π£ = ran πΊ β ((πΉ βΎ π£):π£β1-1-ontoβran
πΉ β (πΉ βΎ ran πΊ):ran πΊβ1-1-ontoβran
πΉ)) |
196 | 195 | rspcev 3613 |
. . 3
β’ ((ran
πΊ β π« π΄ β§ (πΉ βΎ ran πΊ):ran πΊβ1-1-ontoβran
πΉ) β βπ£ β π« π΄(πΉ βΎ π£):π£β1-1-ontoβran
πΉ) |
197 | 39, 191, 196 | syl2anc 585 |
. 2
β’ (π β βπ£ β π« π΄(πΉ βΎ π£):π£β1-1-ontoβran
πΉ) |
198 | | reseq2 5977 |
. . . 4
β’ (π£ = π₯ β (πΉ βΎ π£) = (πΉ βΎ π₯)) |
199 | | id 22 |
. . . 4
β’ (π£ = π₯ β π£ = π₯) |
200 | | eqidd 2734 |
. . . 4
β’ (π£ = π₯ β ran πΉ = ran πΉ) |
201 | 198, 199,
200 | f1oeq123d 6828 |
. . 3
β’ (π£ = π₯ β ((πΉ βΎ π£):π£β1-1-ontoβran
πΉ β (πΉ βΎ π₯):π₯β1-1-ontoβran
πΉ)) |
202 | 201 | cbvrexvw 3236 |
. 2
β’
(βπ£ β
π« π΄(πΉ βΎ π£):π£β1-1-ontoβran
πΉ β βπ₯ β π« π΄(πΉ βΎ π₯):π₯β1-1-ontoβran
πΉ) |
203 | 197, 202 | sylib 217 |
1
β’ (π β βπ₯ β π« π΄(πΉ βΎ π₯):π₯β1-1-ontoβran
πΉ) |