Step | Hyp | Ref
| Expression |
1 | | cfili 24655 |
. . . . . 6
β’ (((πfilGenπ΅) β (CauFilβπ·) β§ π₯ β β+) β
βπ’ β (πfilGenπ΅)βπ§ β π’ βπ€ β π’ (π§π·π€) < π₯) |
2 | 1 | adantll 713 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β§ (πfilGenπ΅) β (CauFilβπ·)) β§ π₯ β β+) β
βπ’ β (πfilGenπ΅)βπ§ β π’ βπ€ β π’ (π§π·π€) < π₯) |
3 | | elfg 23245 |
. . . . . . . 8
β’ (π΅ β (fBasβπ) β (π’ β (πfilGenπ΅) β (π’ β π β§ βπ¦ β π΅ π¦ β π’))) |
4 | 3 | ad3antlr 730 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β§ (πfilGenπ΅) β (CauFilβπ·)) β§ π₯ β β+) β (π’ β (πfilGenπ΅) β (π’ β π β§ βπ¦ β π΅ π¦ β π’))) |
5 | | ssralv 4014 |
. . . . . . . . . . . 12
β’ (π¦ β π’ β (βπ€ β π’ (π§π·π€) < π₯ β βπ€ β π¦ (π§π·π€) < π₯)) |
6 | 5 | ralimdv 3163 |
. . . . . . . . . . 11
β’ (π¦ β π’ β (βπ§ β π’ βπ€ β π’ (π§π·π€) < π₯ β βπ§ β π’ βπ€ β π¦ (π§π·π€) < π₯)) |
7 | | ssralv 4014 |
. . . . . . . . . . 11
β’ (π¦ β π’ β (βπ§ β π’ βπ€ β π¦ (π§π·π€) < π₯ β βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
8 | 6, 7 | syldc 48 |
. . . . . . . . . 10
β’
(βπ§ β
π’ βπ€ β π’ (π§π·π€) < π₯ β (π¦ β π’ β βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
9 | 8 | reximdv 3164 |
. . . . . . . . 9
β’
(βπ§ β
π’ βπ€ β π’ (π§π·π€) < π₯ β (βπ¦ β π΅ π¦ β π’ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
10 | 9 | com12 32 |
. . . . . . . 8
β’
(βπ¦ β
π΅ π¦ β π’ β (βπ§ β π’ βπ€ β π’ (π§π·π€) < π₯ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
11 | 10 | adantl 483 |
. . . . . . 7
β’ ((π’ β π β§ βπ¦ β π΅ π¦ β π’) β (βπ§ β π’ βπ€ β π’ (π§π·π€) < π₯ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
12 | 4, 11 | syl6bi 253 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β§ (πfilGenπ΅) β (CauFilβπ·)) β§ π₯ β β+) β (π’ β (πfilGenπ΅) β (βπ§ β π’ βπ€ β π’ (π§π·π€) < π₯ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯))) |
13 | 12 | rexlimdv 3147 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β§ (πfilGenπ΅) β (CauFilβπ·)) β§ π₯ β β+) β
(βπ’ β (πfilGenπ΅)βπ§ β π’ βπ€ β π’ (π§π·π€) < π₯ β βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
14 | 2, 13 | mpd 15 |
. . . 4
β’ ((((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β§ (πfilGenπ΅) β (CauFilβπ·)) β§ π₯ β β+) β
βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯) |
15 | 14 | ralrimiva 3140 |
. . 3
β’ (((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β§ (πfilGenπ΅) β (CauFilβπ·)) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯) |
16 | 15 | ex 414 |
. 2
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β ((πfilGenπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
17 | | ssfg 23246 |
. . . . . 6
β’ (π΅ β (fBasβπ) β π΅ β (πfilGenπ΅)) |
18 | 17 | adantl 483 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β π΅ β (πfilGenπ΅)) |
19 | | ssrexv 4015 |
. . . . . 6
β’ (π΅ β (πfilGenπ΅) β (βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯ β βπ¦ β (πfilGenπ΅)βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
20 | 19 | ralimdv 3163 |
. . . . 5
β’ (π΅ β (πfilGenπ΅) β (βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯ β βπ₯ β β+ βπ¦ β (πfilGenπ΅)βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
21 | 18, 20 | syl 17 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β (βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯ β βπ₯ β β+ βπ¦ β (πfilGenπ΅)βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |
22 | | fgcl 23252 |
. . . . 5
β’ (π΅ β (fBasβπ) β (πfilGenπ΅) β (Filβπ)) |
23 | 22 | adantl 483 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β (πfilGenπ΅) β (Filβπ)) |
24 | 21, 23 | jctild 527 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β (βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯ β ((πfilGenπ΅) β (Filβπ) β§ βπ₯ β β+ βπ¦ β (πfilGenπ΅)βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯))) |
25 | | iscfil2 24653 |
. . . 4
β’ (π· β (βMetβπ) β ((πfilGenπ΅) β (CauFilβπ·) β ((πfilGenπ΅) β (Filβπ) β§ βπ₯ β β+ βπ¦ β (πfilGenπ΅)βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯))) |
26 | 25 | adantr 482 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β ((πfilGenπ΅) β (CauFilβπ·) β ((πfilGenπ΅) β (Filβπ) β§ βπ₯ β β+ βπ¦ β (πfilGenπ΅)βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯))) |
27 | 24, 26 | sylibrd 259 |
. 2
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β (βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯ β (πfilGenπ΅) β (CauFilβπ·))) |
28 | 16, 27 | impbid 211 |
1
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β ((πfilGenπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) |