Step | Hyp | Ref
| Expression |
1 | | imass2 6058 |
. . . . . . . . . . 11
β’ (π΄ β π΅ β ( M β π΄) β ( M β π΅)) |
2 | 1 | unissd 4879 |
. . . . . . . . . 10
β’ (π΄ β π΅ β βͺ ( M
β π΄) β βͺ ( M β π΅)) |
3 | 2 | sspwd 4577 |
. . . . . . . . 9
β’ (π΄ β π΅ β π« βͺ ( M β π΄) β π« βͺ ( M β π΅)) |
4 | 3 | adantl 483 |
. . . . . . . 8
β’ ((π΅ β On β§ π΄ β π΅) β π« βͺ ( M β π΄) β π« βͺ ( M β π΅)) |
5 | 4 | adantl 483 |
. . . . . . 7
β’ ((π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β π« βͺ ( M β π΄) β π« βͺ ( M β π΅)) |
6 | | ssrexv 4015 |
. . . . . . 7
β’
(π« βͺ ( M β π΄) β π« βͺ ( M β π΅) β (βπ β π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯) β βπ β π« βͺ ( M β π΅)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯))) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ ((π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β (βπ β π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯) β βπ β π« βͺ ( M β π΅)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯))) |
8 | | ssrexv 4015 |
. . . . . . . 8
β’
(π« βͺ ( M β π΄) β π« βͺ ( M β π΅) β (βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯) β βπ β π« βͺ ( M β π΅)(π <<s π β§ (π |s π) = π₯))) |
9 | 5, 8 | syl 17 |
. . . . . . 7
β’ ((π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β (βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯) β βπ β π« βͺ ( M β π΅)(π <<s π β§ (π |s π) = π₯))) |
10 | 9 | reximdv 3164 |
. . . . . 6
β’ ((π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β (βπ β π« βͺ ( M β π΅)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯) β βπ β π« βͺ ( M β π΅)βπ β π« βͺ ( M β π΅)(π <<s π β§ (π |s π) = π₯))) |
11 | 7, 10 | syld 47 |
. . . . 5
β’ ((π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β (βπ β π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯) β βπ β π« βͺ ( M β π΅)βπ β π« βͺ ( M β π΅)(π <<s π β§ (π |s π) = π₯))) |
12 | 11 | adantr 482 |
. . . 4
β’ (((π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β§ π₯ β No )
β (βπ β
π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯) β βπ β π« βͺ ( M β π΅)βπ β π« βͺ ( M β π΅)(π <<s π β§ (π |s π) = π₯))) |
13 | 12 | ss2rabdv 4037 |
. . 3
β’ ((π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β {π₯ β No
β£ βπ β
π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯)} β {π₯ β No
β£ βπ β
π« βͺ ( M β π΅)βπ β π« βͺ ( M β π΅)(π <<s π β§ (π |s π) = π₯)}) |
14 | | madeval2 27212 |
. . . 4
β’ (π΄ β On β ( M
βπ΄) = {π₯ β
No β£ βπ
β π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯)}) |
15 | 14 | adantr 482 |
. . 3
β’ ((π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β ( M βπ΄) = {π₯ β No
β£ βπ β
π« βͺ ( M β π΄)βπ β π« βͺ ( M β π΄)(π <<s π β§ (π |s π) = π₯)}) |
16 | | madeval2 27212 |
. . . . 5
β’ (π΅ β On β ( M
βπ΅) = {π₯ β
No β£ βπ
β π« βͺ ( M β π΅)βπ β π« βͺ ( M β π΅)(π <<s π β§ (π |s π) = π₯)}) |
17 | 16 | adantr 482 |
. . . 4
β’ ((π΅ β On β§ π΄ β π΅) β ( M βπ΅) = {π₯ β No
β£ βπ β
π« βͺ ( M β π΅)βπ β π« βͺ ( M β π΅)(π <<s π β§ (π |s π) = π₯)}) |
18 | 17 | adantl 483 |
. . 3
β’ ((π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β ( M βπ΅) = {π₯ β No
β£ βπ β
π« βͺ ( M β π΅)βπ β π« βͺ ( M β π΅)(π <<s π β§ (π |s π) = π₯)}) |
19 | 13, 15, 18 | 3sstr4d 3995 |
. 2
β’ ((π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β ( M βπ΄) β ( M βπ΅)) |
20 | | madef 27215 |
. . . . . . 7
β’ M
:OnβΆπ« No |
21 | 20 | fdmi 6684 |
. . . . . 6
β’ dom M =
On |
22 | 21 | eleq2i 2826 |
. . . . 5
β’ (π΄ β dom M β π΄ β On) |
23 | | ndmfv 6881 |
. . . . 5
β’ (Β¬
π΄ β dom M β ( M
βπ΄) =
β
) |
24 | 22, 23 | sylnbir 331 |
. . . 4
β’ (Β¬
π΄ β On β ( M
βπ΄) =
β
) |
25 | | 0ss 4360 |
. . . 4
β’ β
β ( M βπ΅) |
26 | 24, 25 | eqsstrdi 4002 |
. . 3
β’ (Β¬
π΄ β On β ( M
βπ΄) β ( M
βπ΅)) |
27 | 26 | adantr 482 |
. 2
β’ ((Β¬
π΄ β On β§ (π΅ β On β§ π΄ β π΅)) β ( M βπ΄) β ( M βπ΅)) |
28 | 19, 27 | pm2.61ian 811 |
1
β’ ((π΅ β On β§ π΄ β π΅) β ( M βπ΄) β ( M βπ΅)) |