Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . . . 8
β’ (π = πΌ β (π€βπ) = (π€βπΌ)) |
2 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = πΌ β (πΉβπ) = (πΉβπΌ)) |
3 | 2 | unieqd 4884 |
. . . . . . . 8
β’ (π = πΌ β βͺ (πΉβπ) = βͺ (πΉβπΌ)) |
4 | 1, 3 | eleq12d 2832 |
. . . . . . 7
β’ (π = πΌ β ((π€βπ) β βͺ (πΉβπ) β (π€βπΌ) β βͺ (πΉβπΌ))) |
5 | | vex 3452 |
. . . . . . . . . . 11
β’ π€ β V |
6 | 5 | elixp 8849 |
. . . . . . . . . 10
β’ (π€ β Xπ β
π΄ βͺ (πΉβπ) β (π€ Fn π΄ β§ βπ β π΄ (π€βπ) β βͺ (πΉβπ))) |
7 | 6 | simprbi 498 |
. . . . . . . . 9
β’ (π€ β Xπ β
π΄ βͺ (πΉβπ) β βπ β π΄ (π€βπ) β βͺ (πΉβπ)) |
8 | | ptpjpre1.1 |
. . . . . . . . 9
β’ π = Xπ β π΄ βͺ (πΉβπ) |
9 | 7, 8 | eleq2s 2856 |
. . . . . . . 8
β’ (π€ β π β βπ β π΄ (π€βπ) β βͺ (πΉβπ)) |
10 | 9 | adantl 483 |
. . . . . . 7
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π€ β π) β βπ β π΄ (π€βπ) β βͺ (πΉβπ)) |
11 | | simplrl 776 |
. . . . . . 7
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π€ β π) β πΌ β π΄) |
12 | 4, 10, 11 | rspcdva 3585 |
. . . . . 6
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π€ β π) β (π€βπΌ) β βͺ (πΉβπΌ)) |
13 | 12 | fmpttd 7068 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (π€ β π β¦ (π€βπΌ)):πβΆβͺ (πΉβπΌ)) |
14 | | ffn 6673 |
. . . . 5
β’ ((π€ β π β¦ (π€βπΌ)):πβΆβͺ (πΉβπΌ) β (π€ β π β¦ (π€βπΌ)) Fn π) |
15 | | elpreima 7013 |
. . . . 5
β’ ((π€ β π β¦ (π€βπΌ)) Fn π β (π§ β (β‘(π€ β π β¦ (π€βπΌ)) β π) β (π§ β π β§ ((π€ β π β¦ (π€βπΌ))βπ§) β π))) |
16 | 13, 14, 15 | 3syl 18 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (π§ β (β‘(π€ β π β¦ (π€βπΌ)) β π) β (π§ β π β§ ((π€ β π β¦ (π€βπΌ))βπ§) β π))) |
17 | | fveq1 6846 |
. . . . . . . . 9
β’ (π€ = π§ β (π€βπΌ) = (π§βπΌ)) |
18 | | eqid 2737 |
. . . . . . . . 9
β’ (π€ β π β¦ (π€βπΌ)) = (π€ β π β¦ (π€βπΌ)) |
19 | | fvex 6860 |
. . . . . . . . 9
β’ (π§βπΌ) β V |
20 | 17, 18, 19 | fvmpt 6953 |
. . . . . . . 8
β’ (π§ β π β ((π€ β π β¦ (π€βπΌ))βπ§) = (π§βπΌ)) |
21 | 20 | eleq1d 2823 |
. . . . . . 7
β’ (π§ β π β (((π€ β π β¦ (π€βπΌ))βπ§) β π β (π§βπΌ) β π)) |
22 | 21 | pm5.32i 576 |
. . . . . 6
β’ ((π§ β π β§ ((π€ β π β¦ (π€βπΌ))βπ§) β π) β (π§ β π β§ (π§βπΌ) β π)) |
23 | 8 | eleq2i 2830 |
. . . . . . . . 9
β’ (π§ β π β π§ β Xπ β π΄ βͺ (πΉβπ)) |
24 | | vex 3452 |
. . . . . . . . . 10
β’ π§ β V |
25 | 24 | elixp 8849 |
. . . . . . . . 9
β’ (π§ β Xπ β
π΄ βͺ (πΉβπ) β (π§ Fn π΄ β§ βπ β π΄ (π§βπ) β βͺ (πΉβπ))) |
26 | 23, 25 | bitri 275 |
. . . . . . . 8
β’ (π§ β π β (π§ Fn π΄ β§ βπ β π΄ (π§βπ) β βͺ (πΉβπ))) |
27 | 26 | anbi1i 625 |
. . . . . . 7
β’ ((π§ β π β§ (π§βπΌ) β π) β ((π§ Fn π΄ β§ βπ β π΄ (π§βπ) β βͺ (πΉβπ)) β§ (π§βπΌ) β π)) |
28 | | anass 470 |
. . . . . . 7
β’ (((π§ Fn π΄ β§ βπ β π΄ (π§βπ) β βͺ (πΉβπ)) β§ (π§βπΌ) β π) β (π§ Fn π΄ β§ (βπ β π΄ (π§βπ) β βͺ (πΉβπ) β§ (π§βπΌ) β π))) |
29 | 27, 28 | bitri 275 |
. . . . . 6
β’ ((π§ β π β§ (π§βπΌ) β π) β (π§ Fn π΄ β§ (βπ β π΄ (π§βπ) β βͺ (πΉβπ) β§ (π§βπΌ) β π))) |
30 | 22, 29 | bitri 275 |
. . . . 5
β’ ((π§ β π β§ ((π€ β π β¦ (π€βπΌ))βπ§) β π) β (π§ Fn π΄ β§ (βπ β π΄ (π§βπ) β βͺ (πΉβπ) β§ (π§βπΌ) β π))) |
31 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ ((π§βπΌ) β π β§ (π§βπ) β βͺ (πΉβπ))) β (π§βπΌ) β π) |
32 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = πΌ β (π§βπ) = (π§βπΌ)) |
33 | | iftrue 4497 |
. . . . . . . . . . . . . 14
β’ (π = πΌ β if(π = πΌ, π, βͺ (πΉβπ)) = π) |
34 | 32, 33 | eleq12d 2832 |
. . . . . . . . . . . . 13
β’ (π = πΌ β ((π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)) β (π§βπΌ) β π)) |
35 | 31, 34 | syl5ibrcom 247 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ ((π§βπΌ) β π β§ (π§βπ) β βͺ (πΉβπ))) β (π = πΌ β (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)))) |
36 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ ((π§βπΌ) β π β§ (π§βπ) β βͺ (πΉβπ))) β (π§βπ) β βͺ (πΉβπ)) |
37 | | iffalse 4500 |
. . . . . . . . . . . . . 14
β’ (Β¬
π = πΌ β if(π = πΌ, π, βͺ (πΉβπ)) = βͺ (πΉβπ)) |
38 | 37 | eleq2d 2824 |
. . . . . . . . . . . . 13
β’ (Β¬
π = πΌ β ((π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)) β (π§βπ) β βͺ (πΉβπ))) |
39 | 36, 38 | syl5ibrcom 247 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ ((π§βπΌ) β π β§ (π§βπ) β βͺ (πΉβπ))) β (Β¬ π = πΌ β (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)))) |
40 | 35, 39 | pm2.61d 179 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ ((π§βπΌ) β π β§ (π§βπ) β βͺ (πΉβπ))) β (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ))) |
41 | 40 | expr 458 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ (π§βπΌ) β π) β ((π§βπ) β βͺ (πΉβπ) β (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)))) |
42 | 41 | ralimdv 3167 |
. . . . . . . . 9
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ (π§βπΌ) β π) β (βπ β π΄ (π§βπ) β βͺ (πΉβπ) β βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)))) |
43 | 42 | expimpd 455 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (((π§βπΌ) β π β§ βπ β π΄ (π§βπ) β βͺ (πΉβπ)) β βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)))) |
44 | 43 | ancomsd 467 |
. . . . . . 7
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β ((βπ β π΄ (π§βπ) β βͺ (πΉβπ) β§ (π§βπΌ) β π) β βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)))) |
45 | | elssuni 4903 |
. . . . . . . . . . . . 13
β’ (π β (πΉβπΌ) β π β βͺ (πΉβπΌ)) |
46 | 45 | ad2antll 728 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β π β βͺ (πΉβπΌ)) |
47 | 33, 3 | sseq12d 3982 |
. . . . . . . . . . . 12
β’ (π = πΌ β (if(π = πΌ, π, βͺ (πΉβπ)) β βͺ
(πΉβπ) β π β βͺ (πΉβπΌ))) |
48 | 46, 47 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (π = πΌ β if(π = πΌ, π, βͺ (πΉβπ)) β βͺ
(πΉβπ))) |
49 | | ssid 3971 |
. . . . . . . . . . . 12
β’ βͺ (πΉβπ) β βͺ (πΉβπ) |
50 | 37, 49 | eqsstrdi 4003 |
. . . . . . . . . . 11
β’ (Β¬
π = πΌ β if(π = πΌ, π, βͺ (πΉβπ)) β βͺ
(πΉβπ)) |
51 | 48, 50 | pm2.61d1 180 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β if(π = πΌ, π, βͺ (πΉβπ)) β βͺ
(πΉβπ)) |
52 | 51 | sseld 3948 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β ((π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)) β (π§βπ) β βͺ (πΉβπ))) |
53 | 52 | ralimdv 3167 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)) β βπ β π΄ (π§βπ) β βͺ (πΉβπ))) |
54 | 34 | rspcv 3580 |
. . . . . . . . 9
β’ (πΌ β π΄ β (βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)) β (π§βπΌ) β π)) |
55 | 54 | ad2antrl 727 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)) β (π§βπΌ) β π)) |
56 | 53, 55 | jcad 514 |
. . . . . . 7
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)) β (βπ β π΄ (π§βπ) β βͺ (πΉβπ) β§ (π§βπΌ) β π))) |
57 | 44, 56 | impbid 211 |
. . . . . 6
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β ((βπ β π΄ (π§βπ) β βͺ (πΉβπ) β§ (π§βπΌ) β π) β βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)))) |
58 | 57 | anbi2d 630 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β ((π§ Fn π΄ β§ (βπ β π΄ (π§βπ) β βͺ (πΉβπ) β§ (π§βπΌ) β π)) β (π§ Fn π΄ β§ βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ))))) |
59 | 30, 58 | bitrid 283 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β ((π§ β π β§ ((π€ β π β¦ (π€βπΌ))βπ§) β π) β (π§ Fn π΄ β§ βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ))))) |
60 | 16, 59 | bitrd 279 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (π§ β (β‘(π€ β π β¦ (π€βπΌ)) β π) β (π§ Fn π΄ β§ βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ))))) |
61 | 24 | elixp 8849 |
. . 3
β’ (π§ β Xπ β
π΄ if(π = πΌ, π, βͺ (πΉβπ)) β (π§ Fn π΄ β§ βπ β π΄ (π§βπ) β if(π = πΌ, π, βͺ (πΉβπ)))) |
62 | 60, 61 | bitr4di 289 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (π§ β (β‘(π€ β π β¦ (π€βπΌ)) β π) β π§ β Xπ β π΄ if(π = πΌ, π, βͺ (πΉβπ)))) |
63 | 62 | eqrdv 2735 |
1
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (β‘(π€ β π β¦ (π€βπΌ)) β π) = Xπ β π΄ if(π = πΌ, π, βͺ (πΉβπ))) |