Step | Hyp | Ref
| Expression |
1 | | fbasrn.c |
. . 3
β’ πΆ = ran (π₯ β π΅ β¦ (πΉ β π₯)) |
2 | | simpl3 1194 |
. . . . . 6
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ π₯ β π΅) β π β π) |
3 | | simpl2 1193 |
. . . . . . 7
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ π₯ β π΅) β πΉ:πβΆπ) |
4 | | fimass 6694 |
. . . . . . 7
β’ (πΉ:πβΆπ β (πΉ β π₯) β π) |
5 | 3, 4 | syl 17 |
. . . . . 6
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ π₯ β π΅) β (πΉ β π₯) β π) |
6 | 2, 5 | sselpwd 5288 |
. . . . 5
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ π₯ β π΅) β (πΉ β π₯) β π« π) |
7 | 6 | fmpttd 7068 |
. . . 4
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β (π₯ β π΅ β¦ (πΉ β π₯)):π΅βΆπ« π) |
8 | 7 | frnd 6681 |
. . 3
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β ran (π₯ β π΅ β¦ (πΉ β π₯)) β π« π) |
9 | 1, 8 | eqsstrid 3997 |
. 2
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β πΆ β π« π) |
10 | 1 | a1i 11 |
. . . 4
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β πΆ = ran (π₯ β π΅ β¦ (πΉ β π₯))) |
11 | | ffun 6676 |
. . . . . . . 8
β’ (πΉ:πβΆπ β Fun πΉ) |
12 | 11 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β Fun πΉ) |
13 | | funimaexg 6592 |
. . . . . . . 8
β’ ((Fun
πΉ β§ π₯ β π΅) β (πΉ β π₯) β V) |
14 | 13 | ralrimiva 3144 |
. . . . . . 7
β’ (Fun
πΉ β βπ₯ β π΅ (πΉ β π₯) β V) |
15 | | dmmptg 6199 |
. . . . . . 7
β’
(βπ₯ β
π΅ (πΉ β π₯) β V β dom (π₯ β π΅ β¦ (πΉ β π₯)) = π΅) |
16 | 12, 14, 15 | 3syl 18 |
. . . . . 6
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β dom (π₯ β π΅ β¦ (πΉ β π₯)) = π΅) |
17 | | fbasne0 23197 |
. . . . . . 7
β’ (π΅ β (fBasβπ) β π΅ β β
) |
18 | 17 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β π΅ β β
) |
19 | 16, 18 | eqnetrd 3012 |
. . . . 5
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β dom (π₯ β π΅ β¦ (πΉ β π₯)) β β
) |
20 | | dm0rn0 5885 |
. . . . . 6
β’ (dom
(π₯ β π΅ β¦ (πΉ β π₯)) = β
β ran (π₯ β π΅ β¦ (πΉ β π₯)) = β
) |
21 | 20 | necon3bii 2997 |
. . . . 5
β’ (dom
(π₯ β π΅ β¦ (πΉ β π₯)) β β
β ran (π₯ β π΅ β¦ (πΉ β π₯)) β β
) |
22 | 19, 21 | sylib 217 |
. . . 4
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β ran (π₯ β π΅ β¦ (πΉ β π₯)) β β
) |
23 | 10, 22 | eqnetrd 3012 |
. . 3
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β πΆ β β
) |
24 | | fbelss 23200 |
. . . . . . . . 9
β’ ((π΅ β (fBasβπ) β§ π₯ β π΅) β π₯ β π) |
25 | 24 | ex 414 |
. . . . . . . 8
β’ (π΅ β (fBasβπ) β (π₯ β π΅ β π₯ β π)) |
26 | 25 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β (π₯ β π΅ β π₯ β π)) |
27 | | 0nelfb 23198 |
. . . . . . . . . 10
β’ (π΅ β (fBasβπ) β Β¬ β
β
π΅) |
28 | | eleq1 2826 |
. . . . . . . . . . 11
β’ (π₯ = β
β (π₯ β π΅ β β
β π΅)) |
29 | 28 | notbid 318 |
. . . . . . . . . 10
β’ (π₯ = β
β (Β¬ π₯ β π΅ β Β¬ β
β π΅)) |
30 | 27, 29 | syl5ibrcom 247 |
. . . . . . . . 9
β’ (π΅ β (fBasβπ) β (π₯ = β
β Β¬ π₯ β π΅)) |
31 | 30 | con2d 134 |
. . . . . . . 8
β’ (π΅ β (fBasβπ) β (π₯ β π΅ β Β¬ π₯ = β
)) |
32 | 31 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β (π₯ β π΅ β Β¬ π₯ = β
)) |
33 | 26, 32 | jcad 514 |
. . . . . 6
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β (π₯ β π΅ β (π₯ β π β§ Β¬ π₯ = β
))) |
34 | | fdm 6682 |
. . . . . . . . . . . . . . 15
β’ (πΉ:πβΆπ β dom πΉ = π) |
35 | 34 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β dom πΉ = π) |
36 | 35 | sseq2d 3981 |
. . . . . . . . . . . . 13
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β (π₯ β dom πΉ β π₯ β π)) |
37 | 36 | biimpar 479 |
. . . . . . . . . . . 12
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ π₯ β π) β π₯ β dom πΉ) |
38 | | sseqin2 4180 |
. . . . . . . . . . . 12
β’ (π₯ β dom πΉ β (dom πΉ β© π₯) = π₯) |
39 | 37, 38 | sylib 217 |
. . . . . . . . . . 11
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ π₯ β π) β (dom πΉ β© π₯) = π₯) |
40 | 39 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ π₯ β π) β ((dom πΉ β© π₯) = β
β π₯ = β
)) |
41 | 40 | biimpd 228 |
. . . . . . . . 9
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ π₯ β π) β ((dom πΉ β© π₯) = β
β π₯ = β
)) |
42 | 41 | con3d 152 |
. . . . . . . 8
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ π₯ β π) β (Β¬ π₯ = β
β Β¬ (dom πΉ β© π₯) = β
)) |
43 | 42 | expimpd 455 |
. . . . . . 7
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β ((π₯ β π β§ Β¬ π₯ = β
) β Β¬ (dom πΉ β© π₯) = β
)) |
44 | | eqcom 2744 |
. . . . . . . . 9
β’ (β
= (πΉ β π₯) β (πΉ β π₯) = β
) |
45 | | imadisj 6037 |
. . . . . . . . 9
β’ ((πΉ β π₯) = β
β (dom πΉ β© π₯) = β
) |
46 | 44, 45 | bitri 275 |
. . . . . . . 8
β’ (β
= (πΉ β π₯) β (dom πΉ β© π₯) = β
) |
47 | 46 | notbii 320 |
. . . . . . 7
β’ (Β¬
β
= (πΉ β π₯) β Β¬ (dom πΉ β© π₯) = β
) |
48 | 43, 47 | syl6ibr 252 |
. . . . . 6
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β ((π₯ β π β§ Β¬ π₯ = β
) β Β¬ β
= (πΉ β π₯))) |
49 | 33, 48 | syld 47 |
. . . . 5
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β (π₯ β π΅ β Β¬ β
= (πΉ β π₯))) |
50 | 49 | ralrimiv 3143 |
. . . 4
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β βπ₯ β π΅ Β¬ β
= (πΉ β π₯)) |
51 | 1 | eleq2i 2830 |
. . . . . . 7
β’ (β
β πΆ β β
β ran (π₯ β π΅ β¦ (πΉ β π₯))) |
52 | | 0ex 5269 |
. . . . . . . 8
β’ β
β V |
53 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β π΅ β¦ (πΉ β π₯)) = (π₯ β π΅ β¦ (πΉ β π₯)) |
54 | 53 | elrnmpt 5916 |
. . . . . . . 8
β’ (β
β V β (β
β ran (π₯ β π΅ β¦ (πΉ β π₯)) β βπ₯ β π΅ β
= (πΉ β π₯))) |
55 | 52, 54 | ax-mp 5 |
. . . . . . 7
β’ (β
β ran (π₯ β π΅ β¦ (πΉ β π₯)) β βπ₯ β π΅ β
= (πΉ β π₯)) |
56 | 51, 55 | bitri 275 |
. . . . . 6
β’ (β
β πΆ β
βπ₯ β π΅ β
= (πΉ β π₯)) |
57 | 56 | notbii 320 |
. . . . 5
β’ (Β¬
β
β πΆ β
Β¬ βπ₯ β π΅ β
= (πΉ β π₯)) |
58 | | df-nel 3051 |
. . . . 5
β’ (β
β πΆ β Β¬
β
β πΆ) |
59 | | ralnex 3076 |
. . . . 5
β’
(βπ₯ β
π΅ Β¬ β
= (πΉ β π₯) β Β¬ βπ₯ β π΅ β
= (πΉ β π₯)) |
60 | 57, 58, 59 | 3bitr4i 303 |
. . . 4
β’ (β
β πΆ β
βπ₯ β π΅ Β¬ β
= (πΉ β π₯)) |
61 | 50, 60 | sylibr 233 |
. . 3
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β β
β πΆ) |
62 | 1 | eleq2i 2830 |
. . . . . . . 8
β’ (π β πΆ β π β ran (π₯ β π΅ β¦ (πΉ β π₯))) |
63 | | imaeq2 6014 |
. . . . . . . . . . 11
β’ (π₯ = π’ β (πΉ β π₯) = (πΉ β π’)) |
64 | 63 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π₯ β π΅ β¦ (πΉ β π₯)) = (π’ β π΅ β¦ (πΉ β π’)) |
65 | 64 | elrnmpt 5916 |
. . . . . . . . 9
β’ (π β V β (π β ran (π₯ β π΅ β¦ (πΉ β π₯)) β βπ’ β π΅ π = (πΉ β π’))) |
66 | 65 | elv 3454 |
. . . . . . . 8
β’ (π β ran (π₯ β π΅ β¦ (πΉ β π₯)) β βπ’ β π΅ π = (πΉ β π’)) |
67 | 62, 66 | bitri 275 |
. . . . . . 7
β’ (π β πΆ β βπ’ β π΅ π = (πΉ β π’)) |
68 | 1 | eleq2i 2830 |
. . . . . . . 8
β’ (π β πΆ β π β ran (π₯ β π΅ β¦ (πΉ β π₯))) |
69 | | imaeq2 6014 |
. . . . . . . . . . 11
β’ (π₯ = π£ β (πΉ β π₯) = (πΉ β π£)) |
70 | 69 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π₯ β π΅ β¦ (πΉ β π₯)) = (π£ β π΅ β¦ (πΉ β π£)) |
71 | 70 | elrnmpt 5916 |
. . . . . . . . 9
β’ (π β V β (π β ran (π₯ β π΅ β¦ (πΉ β π₯)) β βπ£ β π΅ π = (πΉ β π£))) |
72 | 71 | elv 3454 |
. . . . . . . 8
β’ (π β ran (π₯ β π΅ β¦ (πΉ β π₯)) β βπ£ β π΅ π = (πΉ β π£)) |
73 | 68, 72 | bitri 275 |
. . . . . . 7
β’ (π β πΆ β βπ£ β π΅ π = (πΉ β π£)) |
74 | 67, 73 | anbi12i 628 |
. . . . . 6
β’ ((π β πΆ β§ π β πΆ) β (βπ’ β π΅ π = (πΉ β π’) β§ βπ£ β π΅ π = (πΉ β π£))) |
75 | | reeanv 3220 |
. . . . . 6
β’
(βπ’ β
π΅ βπ£ β π΅ (π = (πΉ β π’) β§ π = (πΉ β π£)) β (βπ’ β π΅ π = (πΉ β π’) β§ βπ£ β π΅ π = (πΉ β π£))) |
76 | 74, 75 | bitr4i 278 |
. . . . 5
β’ ((π β πΆ β§ π β πΆ) β βπ’ β π΅ βπ£ β π΅ (π = (πΉ β π’) β§ π = (πΉ β π£))) |
77 | | fbasssin 23203 |
. . . . . . . . . . 11
β’ ((π΅ β (fBasβπ) β§ π’ β π΅ β§ π£ β π΅) β βπ€ β π΅ π€ β (π’ β© π£)) |
78 | 77 | 3expb 1121 |
. . . . . . . . . 10
β’ ((π΅ β (fBasβπ) β§ (π’ β π΅ β§ π£ β π΅)) β βπ€ β π΅ π€ β (π’ β© π£)) |
79 | 78 | 3ad2antl1 1186 |
. . . . . . . . 9
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ (π’ β π΅ β§ π£ β π΅)) β βπ€ β π΅ π€ β (π’ β© π£)) |
80 | 79 | adantrr 716 |
. . . . . . . 8
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ ((π’ β π΅ β§ π£ β π΅) β§ (π = (πΉ β π’) β§ π = (πΉ β π£)))) β βπ€ β π΅ π€ β (π’ β© π£)) |
81 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (πΉ β π€) = (πΉ β π€) |
82 | | imaeq2 6014 |
. . . . . . . . . . . . . 14
β’ (π₯ = π€ β (πΉ β π₯) = (πΉ β π€)) |
83 | 82 | rspceeqv 3600 |
. . . . . . . . . . . . 13
β’ ((π€ β π΅ β§ (πΉ β π€) = (πΉ β π€)) β βπ₯ β π΅ (πΉ β π€) = (πΉ β π₯)) |
84 | 81, 83 | mpan2 690 |
. . . . . . . . . . . 12
β’ (π€ β π΅ β βπ₯ β π΅ (πΉ β π€) = (πΉ β π₯)) |
85 | 84 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ (π = (πΉ β π’) β§ π = (πΉ β π£))) β§ (π€ β π΅ β§ π€ β (π’ β© π£))) β βπ₯ β π΅ (πΉ β π€) = (πΉ β π₯)) |
86 | 1 | eleq2i 2830 |
. . . . . . . . . . . . 13
β’ ((πΉ β π€) β πΆ β (πΉ β π€) β ran (π₯ β π΅ β¦ (πΉ β π₯))) |
87 | | vex 3452 |
. . . . . . . . . . . . . . 15
β’ π€ β V |
88 | 87 | funimaex 6594 |
. . . . . . . . . . . . . 14
β’ (Fun
πΉ β (πΉ β π€) β V) |
89 | 53 | elrnmpt 5916 |
. . . . . . . . . . . . . 14
β’ ((πΉ β π€) β V β ((πΉ β π€) β ran (π₯ β π΅ β¦ (πΉ β π₯)) β βπ₯ β π΅ (πΉ β π€) = (πΉ β π₯))) |
90 | 12, 88, 89 | 3syl 18 |
. . . . . . . . . . . . 13
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β ((πΉ β π€) β ran (π₯ β π΅ β¦ (πΉ β π₯)) β βπ₯ β π΅ (πΉ β π€) = (πΉ β π₯))) |
91 | 86, 90 | bitrid 283 |
. . . . . . . . . . . 12
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β ((πΉ β π€) β πΆ β βπ₯ β π΅ (πΉ β π€) = (πΉ β π₯))) |
92 | 91 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ (π = (πΉ β π’) β§ π = (πΉ β π£))) β§ (π€ β π΅ β§ π€ β (π’ β© π£))) β ((πΉ β π€) β πΆ β βπ₯ β π΅ (πΉ β π€) = (πΉ β π₯))) |
93 | 85, 92 | mpbird 257 |
. . . . . . . . . 10
β’ ((((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ (π = (πΉ β π’) β§ π = (πΉ β π£))) β§ (π€ β π΅ β§ π€ β (π’ β© π£))) β (πΉ β π€) β πΆ) |
94 | | imass2 6059 |
. . . . . . . . . . . 12
β’ (π€ β (π’ β© π£) β (πΉ β π€) β (πΉ β (π’ β© π£))) |
95 | 94 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ (π = (πΉ β π’) β§ π = (πΉ β π£))) β§ (π€ β π΅ β§ π€ β (π’ β© π£))) β (πΉ β π€) β (πΉ β (π’ β© π£))) |
96 | | inss1 4193 |
. . . . . . . . . . . . . 14
β’ (π’ β© π£) β π’ |
97 | | imass2 6059 |
. . . . . . . . . . . . . 14
β’ ((π’ β© π£) β π’ β (πΉ β (π’ β© π£)) β (πΉ β π’)) |
98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (πΉ β (π’ β© π£)) β (πΉ β π’) |
99 | | inss2 4194 |
. . . . . . . . . . . . . 14
β’ (π’ β© π£) β π£ |
100 | | imass2 6059 |
. . . . . . . . . . . . . 14
β’ ((π’ β© π£) β π£ β (πΉ β (π’ β© π£)) β (πΉ β π£)) |
101 | 99, 100 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (πΉ β (π’ β© π£)) β (πΉ β π£) |
102 | 98, 101 | ssini 4196 |
. . . . . . . . . . . 12
β’ (πΉ β (π’ β© π£)) β ((πΉ β π’) β© (πΉ β π£)) |
103 | | ineq12 4172 |
. . . . . . . . . . . . 13
β’ ((π = (πΉ β π’) β§ π = (πΉ β π£)) β (π β© π ) = ((πΉ β π’) β© (πΉ β π£))) |
104 | 103 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ ((((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ (π = (πΉ β π’) β§ π = (πΉ β π£))) β§ (π€ β π΅ β§ π€ β (π’ β© π£))) β (π β© π ) = ((πΉ β π’) β© (πΉ β π£))) |
105 | 102, 104 | sseqtrrid 4002 |
. . . . . . . . . . 11
β’ ((((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ (π = (πΉ β π’) β§ π = (πΉ β π£))) β§ (π€ β π΅ β§ π€ β (π’ β© π£))) β (πΉ β (π’ β© π£)) β (π β© π )) |
106 | 95, 105 | sstrd 3959 |
. . . . . . . . . 10
β’ ((((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ (π = (πΉ β π’) β§ π = (πΉ β π£))) β§ (π€ β π΅ β§ π€ β (π’ β© π£))) β (πΉ β π€) β (π β© π )) |
107 | | sseq1 3974 |
. . . . . . . . . . 11
β’ (π§ = (πΉ β π€) β (π§ β (π β© π ) β (πΉ β π€) β (π β© π ))) |
108 | 107 | rspcev 3584 |
. . . . . . . . . 10
β’ (((πΉ β π€) β πΆ β§ (πΉ β π€) β (π β© π )) β βπ§ β πΆ π§ β (π β© π )) |
109 | 93, 106, 108 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ (π = (πΉ β π’) β§ π = (πΉ β π£))) β§ (π€ β π΅ β§ π€ β (π’ β© π£))) β βπ§ β πΆ π§ β (π β© π )) |
110 | 109 | adantlrl 719 |
. . . . . . . 8
β’ ((((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ ((π’ β π΅ β§ π£ β π΅) β§ (π = (πΉ β π’) β§ π = (πΉ β π£)))) β§ (π€ β π΅ β§ π€ β (π’ β© π£))) β βπ§ β πΆ π§ β (π β© π )) |
111 | 80, 110 | rexlimddv 3159 |
. . . . . . 7
β’ (((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β§ ((π’ β π΅ β§ π£ β π΅) β§ (π = (πΉ β π’) β§ π = (πΉ β π£)))) β βπ§ β πΆ π§ β (π β© π )) |
112 | 111 | exp32 422 |
. . . . . 6
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β ((π’ β π΅ β§ π£ β π΅) β ((π = (πΉ β π’) β§ π = (πΉ β π£)) β βπ§ β πΆ π§ β (π β© π )))) |
113 | 112 | rexlimdvv 3205 |
. . . . 5
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β (βπ’ β π΅ βπ£ β π΅ (π = (πΉ β π’) β§ π = (πΉ β π£)) β βπ§ β πΆ π§ β (π β© π ))) |
114 | 76, 113 | biimtrid 241 |
. . . 4
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β ((π β πΆ β§ π β πΆ) β βπ§ β πΆ π§ β (π β© π ))) |
115 | 114 | ralrimivv 3196 |
. . 3
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β βπ β πΆ βπ β πΆ βπ§ β πΆ π§ β (π β© π )) |
116 | 23, 61, 115 | 3jca 1129 |
. 2
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β (πΆ β β
β§ β
β πΆ β§ βπ β πΆ βπ β πΆ βπ§ β πΆ π§ β (π β© π ))) |
117 | | isfbas2 23202 |
. . 3
β’ (π β π β (πΆ β (fBasβπ) β (πΆ β π« π β§ (πΆ β β
β§ β
β πΆ β§ βπ β πΆ βπ β πΆ βπ§ β πΆ π§ β (π β© π ))))) |
118 | 117 | 3ad2ant3 1136 |
. 2
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β (πΆ β (fBasβπ) β (πΆ β π« π β§ (πΆ β β
β§ β
β πΆ β§ βπ β πΆ βπ β πΆ βπ§ β πΆ π§ β (π β© π ))))) |
119 | 9, 116, 118 | mpbir2and 712 |
1
β’ ((π΅ β (fBasβπ) β§ πΉ:πβΆπ β§ π β π) β πΆ β (fBasβπ)) |