Step | Hyp | Ref
| Expression |
1 | | heiborlem1.4 |
. . . . . . . 8
β’ π΅ β V |
2 | | sseq1 3967 |
. . . . . . . . . 10
β’ (π’ = π΅ β (π’ β βͺ π£ β π΅ β βͺ π£)) |
3 | 2 | rexbidv 3173 |
. . . . . . . . 9
β’ (π’ = π΅ β (βπ£ β (π« π β© Fin)π’ β βͺ π£ β βπ£ β (π« π β© Fin)π΅ β βͺ π£)) |
4 | 3 | notbid 317 |
. . . . . . . 8
β’ (π’ = π΅ β (Β¬ βπ£ β (π« π β© Fin)π’ β βͺ π£ β Β¬ βπ£ β (π« π β© Fin)π΅ β βͺ π£)) |
5 | | heibor.3 |
. . . . . . . 8
β’ πΎ = {π’ β£ Β¬ βπ£ β (π« π β© Fin)π’ β βͺ π£} |
6 | 1, 4, 5 | elab2 3632 |
. . . . . . 7
β’ (π΅ β πΎ β Β¬ βπ£ β (π« π β© Fin)π΅ β βͺ π£) |
7 | 6 | con2bii 357 |
. . . . . 6
β’
(βπ£ β
(π« π β©
Fin)π΅ β βͺ π£
β Β¬ π΅ β πΎ) |
8 | 7 | ralbii 3094 |
. . . . 5
β’
(βπ₯ β
π΄ βπ£ β (π« π β© Fin)π΅ β βͺ π£ β βπ₯ β π΄ Β¬ π΅ β πΎ) |
9 | | ralnex 3073 |
. . . . 5
β’
(βπ₯ β
π΄ Β¬ π΅ β πΎ β Β¬ βπ₯ β π΄ π΅ β πΎ) |
10 | 8, 9 | bitr2i 275 |
. . . 4
β’ (Β¬
βπ₯ β π΄ π΅ β πΎ β βπ₯ β π΄ βπ£ β (π« π β© Fin)π΅ β βͺ π£) |
11 | | unieq 4874 |
. . . . . . . . 9
β’ (π£ = (π‘βπ₯) β βͺ π£ = βͺ
(π‘βπ₯)) |
12 | 11 | sseq2d 3974 |
. . . . . . . 8
β’ (π£ = (π‘βπ₯) β (π΅ β βͺ π£ β π΅ β βͺ (π‘βπ₯))) |
13 | 12 | ac6sfi 9189 |
. . . . . . 7
β’ ((π΄ β Fin β§ βπ₯ β π΄ βπ£ β (π« π β© Fin)π΅ β βͺ π£) β βπ‘(π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) |
14 | 13 | ex 413 |
. . . . . 6
β’ (π΄ β Fin β
(βπ₯ β π΄ βπ£ β (π« π β© Fin)π΅ β βͺ π£ β βπ‘(π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯)))) |
15 | 14 | adantr 481 |
. . . . 5
β’ ((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β (βπ₯ β π΄ βπ£ β (π« π β© Fin)π΅ β βͺ π£ β βπ‘(π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯)))) |
16 | | sseq1 3967 |
. . . . . . . . . . . 12
β’ (π’ = πΆ β (π’ β βͺ π£ β πΆ β βͺ π£)) |
17 | 16 | rexbidv 3173 |
. . . . . . . . . . 11
β’ (π’ = πΆ β (βπ£ β (π« π β© Fin)π’ β βͺ π£ β βπ£ β (π« π β© Fin)πΆ β βͺ π£)) |
18 | 17 | notbid 317 |
. . . . . . . . . 10
β’ (π’ = πΆ β (Β¬ βπ£ β (π« π β© Fin)π’ β βͺ π£ β Β¬ βπ£ β (π« π β© Fin)πΆ β βͺ π£)) |
19 | 18, 5 | elab2g 3630 |
. . . . . . . . 9
β’ (πΆ β πΎ β (πΆ β πΎ β Β¬ βπ£ β (π« π β© Fin)πΆ β βͺ π£)) |
20 | 19 | ibi 266 |
. . . . . . . 8
β’ (πΆ β πΎ β Β¬ βπ£ β (π« π β© Fin)πΆ β βͺ π£) |
21 | | frn 6672 |
. . . . . . . . . . . . . . 15
β’ (π‘:π΄βΆ(π« π β© Fin) β ran π‘ β (π« π β© Fin)) |
22 | 21 | ad2antrl 726 |
. . . . . . . . . . . . . 14
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β ran π‘ β (π« π β© Fin)) |
23 | | inss1 4186 |
. . . . . . . . . . . . . 14
β’
(π« π β©
Fin) β π« π |
24 | 22, 23 | sstrdi 3954 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β ran π‘ β π« π) |
25 | | sspwuni 5058 |
. . . . . . . . . . . . 13
β’ (ran
π‘ β π« π β βͺ ran π‘ β π) |
26 | 24, 25 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β βͺ ran
π‘ β π) |
27 | | vex 3447 |
. . . . . . . . . . . . . . 15
β’ π‘ β V |
28 | 27 | rnex 7841 |
. . . . . . . . . . . . . 14
β’ ran π‘ β V |
29 | 28 | uniex 7670 |
. . . . . . . . . . . . 13
β’ βͺ ran π‘ β V |
30 | 29 | elpw 4562 |
. . . . . . . . . . . 12
β’ (βͺ ran π‘ β π« π β βͺ ran
π‘ β π) |
31 | 26, 30 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β βͺ ran
π‘ β π« π) |
32 | | ffn 6665 |
. . . . . . . . . . . . . . 15
β’ (π‘:π΄βΆ(π« π β© Fin) β π‘ Fn π΄) |
33 | 32 | ad2antrl 726 |
. . . . . . . . . . . . . 14
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β π‘ Fn π΄) |
34 | | dffn4 6759 |
. . . . . . . . . . . . . 14
β’ (π‘ Fn π΄ β π‘:π΄βontoβran π‘) |
35 | 33, 34 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β π‘:π΄βontoβran π‘) |
36 | | fofi 9240 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ π‘:π΄βontoβran π‘) β ran π‘ β Fin) |
37 | 35, 36 | syldan 591 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β ran π‘ β Fin) |
38 | | inss2 4187 |
. . . . . . . . . . . . 13
β’
(π« π β©
Fin) β Fin |
39 | 22, 38 | sstrdi 3954 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β ran π‘ β Fin) |
40 | | unifi 9243 |
. . . . . . . . . . . 12
β’ ((ran
π‘ β Fin β§ ran
π‘ β Fin) β βͺ ran π‘ β Fin) |
41 | 37, 39, 40 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β βͺ ran
π‘ β
Fin) |
42 | 31, 41 | elind 4152 |
. . . . . . . . . 10
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β βͺ ran
π‘ β (π« π β© Fin)) |
43 | 42 | adantlr 713 |
. . . . . . . . 9
β’ (((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β βͺ ran
π‘ β (π« π β© Fin)) |
44 | | simplr 767 |
. . . . . . . . . 10
β’ (((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β πΆ β βͺ
π₯ β π΄ π΅) |
45 | | fnfvelrn 7028 |
. . . . . . . . . . . . . . . . . 18
β’ ((π‘ Fn π΄ β§ π₯ β π΄) β (π‘βπ₯) β ran π‘) |
46 | 32, 45 | sylan 580 |
. . . . . . . . . . . . . . . . 17
β’ ((π‘:π΄βΆ(π« π β© Fin) β§ π₯ β π΄) β (π‘βπ₯) β ran π‘) |
47 | 46 | adantll 712 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β Fin β§ π‘:π΄βΆ(π« π β© Fin)) β§ π₯ β π΄) β (π‘βπ₯) β ran π‘) |
48 | | elssuni 4896 |
. . . . . . . . . . . . . . . 16
β’ ((π‘βπ₯) β ran π‘ β (π‘βπ₯) β βͺ ran
π‘) |
49 | | uniss 4871 |
. . . . . . . . . . . . . . . 16
β’ ((π‘βπ₯) β βͺ ran
π‘ β βͺ (π‘βπ₯) β βͺ βͺ ran π‘) |
50 | 47, 48, 49 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β Fin β§ π‘:π΄βΆ(π« π β© Fin)) β§ π₯ β π΄) β βͺ (π‘βπ₯) β βͺ βͺ ran π‘) |
51 | | sstr2 3949 |
. . . . . . . . . . . . . . 15
β’ (π΅ β βͺ (π‘βπ₯) β (βͺ (π‘βπ₯) β βͺ βͺ ran π‘ β π΅ β βͺ βͺ ran π‘)) |
52 | 50, 51 | syl5com 31 |
. . . . . . . . . . . . . 14
β’ (((π΄ β Fin β§ π‘:π΄βΆ(π« π β© Fin)) β§ π₯ β π΄) β (π΅ β βͺ (π‘βπ₯) β π΅ β βͺ βͺ ran π‘)) |
53 | 52 | ralimdva 3162 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ π‘:π΄βΆ(π« π β© Fin)) β (βπ₯ β π΄ π΅ β βͺ (π‘βπ₯) β βπ₯ β π΄ π΅ β βͺ βͺ ran π‘)) |
54 | 53 | impr 455 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β βπ₯ β π΄ π΅ β βͺ βͺ ran π‘) |
55 | | iunss 5003 |
. . . . . . . . . . . 12
β’ (βͺ π₯ β π΄ π΅ β βͺ βͺ ran π‘ β βπ₯ β π΄ π΅ β βͺ βͺ ran π‘) |
56 | 54, 55 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π΄ β Fin β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β βͺ π₯ β π΄ π΅ β βͺ βͺ ran π‘) |
57 | 56 | adantlr 713 |
. . . . . . . . . 10
β’ (((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β βͺ π₯ β π΄ π΅ β βͺ βͺ ran π‘) |
58 | 44, 57 | sstrd 3952 |
. . . . . . . . 9
β’ (((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β πΆ β βͺ βͺ ran π‘) |
59 | | unieq 4874 |
. . . . . . . . . . 11
β’ (π£ = βͺ
ran π‘ β βͺ π£ =
βͺ βͺ ran π‘) |
60 | 59 | sseq2d 3974 |
. . . . . . . . . 10
β’ (π£ = βͺ
ran π‘ β (πΆ β βͺ π£
β πΆ β βͺ βͺ ran π‘)) |
61 | 60 | rspcev 3579 |
. . . . . . . . 9
β’ ((βͺ ran π‘ β (π« π β© Fin) β§ πΆ β βͺ βͺ ran π‘) β βπ£ β (π« π β© Fin)πΆ β βͺ π£) |
62 | 43, 58, 61 | syl2anc 584 |
. . . . . . . 8
β’ (((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β βπ£ β (π« π β© Fin)πΆ β βͺ π£) |
63 | 20, 62 | nsyl3 138 |
. . . . . . 7
β’ (((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β§ (π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯))) β Β¬ πΆ β πΎ) |
64 | 63 | ex 413 |
. . . . . 6
β’ ((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β ((π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯)) β Β¬ πΆ β πΎ)) |
65 | 64 | exlimdv 1936 |
. . . . 5
β’ ((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β (βπ‘(π‘:π΄βΆ(π« π β© Fin) β§ βπ₯ β π΄ π΅ β βͺ (π‘βπ₯)) β Β¬ πΆ β πΎ)) |
66 | 15, 65 | syld 47 |
. . . 4
β’ ((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β (βπ₯ β π΄ βπ£ β (π« π β© Fin)π΅ β βͺ π£ β Β¬ πΆ β πΎ)) |
67 | 10, 66 | biimtrid 241 |
. . 3
β’ ((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β (Β¬ βπ₯ β π΄ π΅ β πΎ β Β¬ πΆ β πΎ)) |
68 | 67 | con4d 115 |
. 2
β’ ((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅) β (πΆ β πΎ β βπ₯ β π΄ π΅ β πΎ)) |
69 | 68 | 3impia 1117 |
1
β’ ((π΄ β Fin β§ πΆ β βͺ π₯ β π΄ π΅ β§ πΆ β πΎ) β βπ₯ β π΄ π΅ β πΎ) |