Step | Hyp | Ref
| Expression |
1 | | suppcoss.f |
. . . 4
β’ (π β πΉ Fn π΄) |
2 | | dffn3 6685 |
. . . 4
β’ (πΉ Fn π΄ β πΉ:π΄βΆran πΉ) |
3 | 1, 2 | sylib 217 |
. . 3
β’ (π β πΉ:π΄βΆran πΉ) |
4 | | suppcoss.g |
. . 3
β’ (π β πΊ:π΅βΆπ΄) |
5 | 3, 4 | fcod 6698 |
. 2
β’ (π β (πΉ β πΊ):π΅βΆran πΉ) |
6 | | eldif 3924 |
. . . . 5
β’ (π β (π΅ β (πΊ supp π)) β (π β π΅ β§ Β¬ π β (πΊ supp π))) |
7 | 4 | ffnd 6673 |
. . . . . . . . 9
β’ (π β πΊ Fn π΅) |
8 | | suppcoss.b |
. . . . . . . . 9
β’ (π β π΅ β π) |
9 | | suppcoss.y |
. . . . . . . . 9
β’ (π β π β π) |
10 | | elsuppfn 8106 |
. . . . . . . . 9
β’ ((πΊ Fn π΅ β§ π΅ β π β§ π β π) β (π β (πΊ supp π) β (π β π΅ β§ (πΊβπ) β π))) |
11 | 7, 8, 9, 10 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π β (πΊ supp π) β (π β π΅ β§ (πΊβπ) β π))) |
12 | 11 | notbid 318 |
. . . . . . 7
β’ (π β (Β¬ π β (πΊ supp π) β Β¬ (π β π΅ β§ (πΊβπ) β π))) |
13 | 12 | anbi2d 630 |
. . . . . 6
β’ (π β ((π β π΅ β§ Β¬ π β (πΊ supp π)) β (π β π΅ β§ Β¬ (π β π΅ β§ (πΊβπ) β π)))) |
14 | | annotanannot 834 |
. . . . . 6
β’ ((π β π΅ β§ Β¬ (π β π΅ β§ (πΊβπ) β π)) β (π β π΅ β§ Β¬ (πΊβπ) β π)) |
15 | 13, 14 | bitrdi 287 |
. . . . 5
β’ (π β ((π β π΅ β§ Β¬ π β (πΊ supp π)) β (π β π΅ β§ Β¬ (πΊβπ) β π))) |
16 | 6, 15 | bitrid 283 |
. . . 4
β’ (π β (π β (π΅ β (πΊ supp π)) β (π β π΅ β§ Β¬ (πΊβπ) β π))) |
17 | | nne 2944 |
. . . . . 6
β’ (Β¬
(πΊβπ) β π β (πΊβπ) = π) |
18 | 17 | anbi2i 624 |
. . . . 5
β’ ((π β π΅ β§ Β¬ (πΊβπ) β π) β (π β π΅ β§ (πΊβπ) = π)) |
19 | 4 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ (πΊβπ) = π)) β πΊ:π΅βΆπ΄) |
20 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ (πΊβπ) = π)) β π β π΅) |
21 | 19, 20 | fvco3d 6945 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ (πΊβπ) = π)) β ((πΉ β πΊ)βπ) = (πΉβ(πΊβπ))) |
22 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π β π΅ β§ (πΊβπ) = π)) β (πΊβπ) = π) |
23 | 22 | fveq2d 6850 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ (πΊβπ) = π)) β (πΉβ(πΊβπ)) = (πΉβπ)) |
24 | | suppcoss.1 |
. . . . . . . 8
β’ (π β (πΉβπ) = π) |
25 | 24 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β π΅ β§ (πΊβπ) = π)) β (πΉβπ) = π) |
26 | 21, 23, 25 | 3eqtrd 2777 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ (πΊβπ) = π)) β ((πΉ β πΊ)βπ) = π) |
27 | 26 | ex 414 |
. . . . 5
β’ (π β ((π β π΅ β§ (πΊβπ) = π) β ((πΉ β πΊ)βπ) = π)) |
28 | 18, 27 | biimtrid 241 |
. . . 4
β’ (π β ((π β π΅ β§ Β¬ (πΊβπ) β π) β ((πΉ β πΊ)βπ) = π)) |
29 | 16, 28 | sylbid 239 |
. . 3
β’ (π β (π β (π΅ β (πΊ supp π)) β ((πΉ β πΊ)βπ) = π)) |
30 | 29 | imp 408 |
. 2
β’ ((π β§ π β (π΅ β (πΊ supp π))) β ((πΉ β πΊ)βπ) = π) |
31 | 5, 30 | suppss 8129 |
1
β’ (π β ((πΉ β πΊ) supp π) β (πΊ supp π)) |