Step | Hyp | Ref
| Expression |
1 | | fmfnfm.l |
. . . . . . . 8
β’ (π β πΏ β (Filβπ)) |
2 | | filin 23680 |
. . . . . . . . 9
β’ ((πΏ β (Filβπ) β§ π¦ β πΏ β§ π§ β πΏ) β (π¦ β© π§) β πΏ) |
3 | 2 | 3expb 1117 |
. . . . . . . 8
β’ ((πΏ β (Filβπ) β§ (π¦ β πΏ β§ π§ β πΏ)) β (π¦ β© π§) β πΏ) |
4 | 1, 3 | sylan 579 |
. . . . . . 7
β’ ((π β§ (π¦ β πΏ β§ π§ β πΏ)) β (π¦ β© π§) β πΏ) |
5 | | fmfnfm.f |
. . . . . . . . 9
β’ (π β πΉ:πβΆπ) |
6 | | ffun 6710 |
. . . . . . . . 9
β’ (πΉ:πβΆπ β Fun πΉ) |
7 | | funcnvcnv 6605 |
. . . . . . . . 9
β’ (Fun
πΉ β Fun β‘β‘πΉ) |
8 | | imain 6623 |
. . . . . . . . . 10
β’ (Fun
β‘β‘πΉ β (β‘πΉ β (π¦ β© π§)) = ((β‘πΉ β π¦) β© (β‘πΉ β π§))) |
9 | 8 | eqcomd 2730 |
. . . . . . . . 9
β’ (Fun
β‘β‘πΉ β ((β‘πΉ β π¦) β© (β‘πΉ β π§)) = (β‘πΉ β (π¦ β© π§))) |
10 | 5, 6, 7, 9 | 4syl 19 |
. . . . . . . 8
β’ (π β ((β‘πΉ β π¦) β© (β‘πΉ β π§)) = (β‘πΉ β (π¦ β© π§))) |
11 | 10 | adantr 480 |
. . . . . . 7
β’ ((π β§ (π¦ β πΏ β§ π§ β πΏ)) β ((β‘πΉ β π¦) β© (β‘πΉ β π§)) = (β‘πΉ β (π¦ β© π§))) |
12 | | imaeq2 6045 |
. . . . . . . 8
β’ (π₯ = (π¦ β© π§) β (β‘πΉ β π₯) = (β‘πΉ β (π¦ β© π§))) |
13 | 12 | rspceeqv 3625 |
. . . . . . 7
β’ (((π¦ β© π§) β πΏ β§ ((β‘πΉ β π¦) β© (β‘πΉ β π§)) = (β‘πΉ β (π¦ β© π§))) β βπ₯ β πΏ ((β‘πΉ β π¦) β© (β‘πΉ β π§)) = (β‘πΉ β π₯)) |
14 | 4, 11, 13 | syl2anc 583 |
. . . . . 6
β’ ((π β§ (π¦ β πΏ β§ π§ β πΏ)) β βπ₯ β πΏ ((β‘πΉ β π¦) β© (β‘πΉ β π§)) = (β‘πΉ β π₯)) |
15 | | ineq12 4199 |
. . . . . . . 8
β’ ((π = (β‘πΉ β π¦) β§ π‘ = (β‘πΉ β π§)) β (π β© π‘) = ((β‘πΉ β π¦) β© (β‘πΉ β π§))) |
16 | 15 | eqeq1d 2726 |
. . . . . . 7
β’ ((π = (β‘πΉ β π¦) β§ π‘ = (β‘πΉ β π§)) β ((π β© π‘) = (β‘πΉ β π₯) β ((β‘πΉ β π¦) β© (β‘πΉ β π§)) = (β‘πΉ β π₯))) |
17 | 16 | rexbidv 3170 |
. . . . . 6
β’ ((π = (β‘πΉ β π¦) β§ π‘ = (β‘πΉ β π§)) β (βπ₯ β πΏ (π β© π‘) = (β‘πΉ β π₯) β βπ₯ β πΏ ((β‘πΉ β π¦) β© (β‘πΉ β π§)) = (β‘πΉ β π₯))) |
18 | 14, 17 | syl5ibrcom 246 |
. . . . 5
β’ ((π β§ (π¦ β πΏ β§ π§ β πΏ)) β ((π = (β‘πΉ β π¦) β§ π‘ = (β‘πΉ β π§)) β βπ₯ β πΏ (π β© π‘) = (β‘πΉ β π₯))) |
19 | 18 | rexlimdvva 3203 |
. . . 4
β’ (π β (βπ¦ β πΏ βπ§ β πΏ (π = (β‘πΉ β π¦) β§ π‘ = (β‘πΉ β π§)) β βπ₯ β πΏ (π β© π‘) = (β‘πΉ β π₯))) |
20 | | imaeq2 6045 |
. . . . . . . 8
β’ (π₯ = π¦ β (β‘πΉ β π₯) = (β‘πΉ β π¦)) |
21 | 20 | eqeq2d 2735 |
. . . . . . 7
β’ (π₯ = π¦ β (π = (β‘πΉ β π₯) β π = (β‘πΉ β π¦))) |
22 | 21 | cbvrexvw 3227 |
. . . . . 6
β’
(βπ₯ β
πΏ π = (β‘πΉ β π₯) β βπ¦ β πΏ π = (β‘πΉ β π¦)) |
23 | | imaeq2 6045 |
. . . . . . . 8
β’ (π₯ = π§ β (β‘πΉ β π₯) = (β‘πΉ β π§)) |
24 | 23 | eqeq2d 2735 |
. . . . . . 7
β’ (π₯ = π§ β (π‘ = (β‘πΉ β π₯) β π‘ = (β‘πΉ β π§))) |
25 | 24 | cbvrexvw 3227 |
. . . . . 6
β’
(βπ₯ β
πΏ π‘ = (β‘πΉ β π₯) β βπ§ β πΏ π‘ = (β‘πΉ β π§)) |
26 | 22, 25 | anbi12i 626 |
. . . . 5
β’
((βπ₯ β
πΏ π = (β‘πΉ β π₯) β§ βπ₯ β πΏ π‘ = (β‘πΉ β π₯)) β (βπ¦ β πΏ π = (β‘πΉ β π¦) β§ βπ§ β πΏ π‘ = (β‘πΉ β π§))) |
27 | | eqid 2724 |
. . . . . . . 8
β’ (π₯ β πΏ β¦ (β‘πΉ β π₯)) = (π₯ β πΏ β¦ (β‘πΉ β π₯)) |
28 | 27 | elrnmpt 5945 |
. . . . . . 7
β’ (π β V β (π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ π = (β‘πΉ β π₯))) |
29 | 28 | elv 3472 |
. . . . . 6
β’ (π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ π = (β‘πΉ β π₯)) |
30 | 27 | elrnmpt 5945 |
. . . . . . 7
β’ (π‘ β V β (π‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ π‘ = (β‘πΉ β π₯))) |
31 | 30 | elv 3472 |
. . . . . 6
β’ (π‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ π‘ = (β‘πΉ β π₯)) |
32 | 29, 31 | anbi12i 626 |
. . . . 5
β’ ((π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β§ π‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β (βπ₯ β πΏ π = (β‘πΉ β π₯) β§ βπ₯ β πΏ π‘ = (β‘πΉ β π₯))) |
33 | | reeanv 3218 |
. . . . 5
β’
(βπ¦ β
πΏ βπ§ β πΏ (π = (β‘πΉ β π¦) β§ π‘ = (β‘πΉ β π§)) β (βπ¦ β πΏ π = (β‘πΉ β π¦) β§ βπ§ β πΏ π‘ = (β‘πΉ β π§))) |
34 | 26, 32, 33 | 3bitr4i 303 |
. . . 4
β’ ((π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β§ π‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β βπ¦ β πΏ βπ§ β πΏ (π = (β‘πΉ β π¦) β§ π‘ = (β‘πΉ β π§))) |
35 | | vex 3470 |
. . . . . 6
β’ π β V |
36 | 35 | inex1 5307 |
. . . . 5
β’ (π β© π‘) β V |
37 | 27 | elrnmpt 5945 |
. . . . 5
β’ ((π β© π‘) β V β ((π β© π‘) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ (π β© π‘) = (β‘πΉ β π₯))) |
38 | 36, 37 | ax-mp 5 |
. . . 4
β’ ((π β© π‘) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ (π β© π‘) = (β‘πΉ β π₯)) |
39 | 19, 34, 38 | 3imtr4g 296 |
. . 3
β’ (π β ((π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β§ π‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β (π β© π‘) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) |
40 | 39 | ralrimivv 3190 |
. 2
β’ (π β βπ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))βπ‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))(π β© π‘) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) |
41 | | mptexg 7214 |
. . 3
β’ (πΏ β (Filβπ) β (π₯ β πΏ β¦ (β‘πΉ β π₯)) β V) |
42 | | rnexg 7888 |
. . 3
β’ ((π₯ β πΏ β¦ (β‘πΉ β π₯)) β V β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β V) |
43 | | inficl 9416 |
. . 3
β’ (ran
(π₯ β πΏ β¦ (β‘πΉ β π₯)) β V β (βπ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))βπ‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))(π β© π‘) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) = ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) |
44 | 1, 41, 42, 43 | 4syl 19 |
. 2
β’ (π β (βπ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))βπ‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))(π β© π‘) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) = ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) |
45 | 40, 44 | mpbid 231 |
1
β’ (π β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) = ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) |