Step | Hyp | Ref
| Expression |
1 | | r0weon.1 |
. . . . 5
β’ π
= {β¨π§, π€β© β£ ((π§ β (On Γ On) β§ π€ β (On Γ On)) β§
(((1st βπ§)
βͺ (2nd βπ§)) β ((1st βπ€) βͺ (2nd
βπ€)) β¨
(((1st βπ§)
βͺ (2nd βπ§)) = ((1st βπ€) βͺ (2nd
βπ€)) β§ π§πΏπ€)))} |
2 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β (1st βπ₯) = (1st βπ§)) |
3 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β (2nd βπ₯) = (2nd βπ§)) |
4 | 2, 3 | uneq12d 4125 |
. . . . . . . . . . 11
β’ (π₯ = π§ β ((1st βπ₯) βͺ (2nd
βπ₯)) =
((1st βπ§)
βͺ (2nd βπ§))) |
5 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) = (π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) |
6 | | fvex 6856 |
. . . . . . . . . . . 12
β’
(1st βπ§) β V |
7 | | fvex 6856 |
. . . . . . . . . . . 12
β’
(2nd βπ§) β V |
8 | 6, 7 | unex 7681 |
. . . . . . . . . . 11
β’
((1st βπ§) βͺ (2nd βπ§)) β V |
9 | 4, 5, 8 | fvmpt 6949 |
. . . . . . . . . 10
β’ (π§ β (On Γ On) β
((π₯ β (On Γ On)
β¦ ((1st βπ₯) βͺ (2nd βπ₯)))βπ§) = ((1st βπ§) βͺ (2nd
βπ§))) |
10 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β (1st βπ₯) = (1st βπ€)) |
11 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β (2nd βπ₯) = (2nd βπ€)) |
12 | 10, 11 | uneq12d 4125 |
. . . . . . . . . . 11
β’ (π₯ = π€ β ((1st βπ₯) βͺ (2nd
βπ₯)) =
((1st βπ€)
βͺ (2nd βπ€))) |
13 | | fvex 6856 |
. . . . . . . . . . . 12
β’
(1st βπ€) β V |
14 | | fvex 6856 |
. . . . . . . . . . . 12
β’
(2nd βπ€) β V |
15 | 13, 14 | unex 7681 |
. . . . . . . . . . 11
β’
((1st βπ€) βͺ (2nd βπ€)) β V |
16 | 12, 5, 15 | fvmpt 6949 |
. . . . . . . . . 10
β’ (π€ β (On Γ On) β
((π₯ β (On Γ On)
β¦ ((1st βπ₯) βͺ (2nd βπ₯)))βπ€) = ((1st βπ€) βͺ (2nd
βπ€))) |
17 | 9, 16 | breqan12d 5122 |
. . . . . . . . 9
β’ ((π§ β (On Γ On) β§
π€ β (On Γ On))
β (((π₯ β (On
Γ On) β¦ ((1st βπ₯) βͺ (2nd βπ₯)))βπ§) E ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β ((1st βπ§) βͺ (2nd
βπ§)) E
((1st βπ€)
βͺ (2nd βπ€)))) |
18 | 15 | epeli 5540 |
. . . . . . . . 9
β’
(((1st βπ§) βͺ (2nd βπ§)) E ((1st
βπ€) βͺ
(2nd βπ€))
β ((1st βπ§) βͺ (2nd βπ§)) β ((1st
βπ€) βͺ
(2nd βπ€))) |
19 | 17, 18 | bitrdi 287 |
. . . . . . . 8
β’ ((π§ β (On Γ On) β§
π€ β (On Γ On))
β (((π₯ β (On
Γ On) β¦ ((1st βπ₯) βͺ (2nd βπ₯)))βπ§) E ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β ((1st βπ§) βͺ (2nd
βπ§)) β
((1st βπ€)
βͺ (2nd βπ€)))) |
20 | 9, 16 | eqeqan12d 2747 |
. . . . . . . . 9
β’ ((π§ β (On Γ On) β§
π€ β (On Γ On))
β (((π₯ β (On
Γ On) β¦ ((1st βπ₯) βͺ (2nd βπ₯)))βπ§) = ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β ((1st βπ§) βͺ (2nd
βπ§)) =
((1st βπ€)
βͺ (2nd βπ€)))) |
21 | 20 | anbi1d 631 |
. . . . . . . 8
β’ ((π§ β (On Γ On) β§
π€ β (On Γ On))
β ((((π₯ β (On
Γ On) β¦ ((1st βπ₯) βͺ (2nd βπ₯)))βπ§) = ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β§ π§πΏπ€) β (((1st βπ§) βͺ (2nd
βπ§)) =
((1st βπ€)
βͺ (2nd βπ€)) β§ π§πΏπ€))) |
22 | 19, 21 | orbi12d 918 |
. . . . . . 7
β’ ((π§ β (On Γ On) β§
π€ β (On Γ On))
β ((((π₯ β (On
Γ On) β¦ ((1st βπ₯) βͺ (2nd βπ₯)))βπ§) E ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β¨ (((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ§) = ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β§ π§πΏπ€)) β (((1st βπ§) βͺ (2nd
βπ§)) β
((1st βπ€)
βͺ (2nd βπ€)) β¨ (((1st βπ§) βͺ (2nd
βπ§)) =
((1st βπ€)
βͺ (2nd βπ€)) β§ π§πΏπ€)))) |
23 | 22 | pm5.32i 576 |
. . . . . 6
β’ (((π§ β (On Γ On) β§
π€ β (On Γ On))
β§ (((π₯ β (On
Γ On) β¦ ((1st βπ₯) βͺ (2nd βπ₯)))βπ§) E ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β¨ (((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ§) = ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β§ π§πΏπ€))) β ((π§ β (On Γ On) β§ π€ β (On Γ On)) β§
(((1st βπ§)
βͺ (2nd βπ§)) β ((1st βπ€) βͺ (2nd
βπ€)) β¨
(((1st βπ§)
βͺ (2nd βπ§)) = ((1st βπ€) βͺ (2nd
βπ€)) β§ π§πΏπ€)))) |
24 | 23 | opabbii 5173 |
. . . . 5
β’
{β¨π§, π€β© β£ ((π§ β (On Γ On) β§
π€ β (On Γ On))
β§ (((π₯ β (On
Γ On) β¦ ((1st βπ₯) βͺ (2nd βπ₯)))βπ§) E ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β¨ (((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ§) = ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β§ π§πΏπ€)))} = {β¨π§, π€β© β£ ((π§ β (On Γ On) β§ π€ β (On Γ On)) β§
(((1st βπ§)
βͺ (2nd βπ§)) β ((1st βπ€) βͺ (2nd
βπ€)) β¨
(((1st βπ§)
βͺ (2nd βπ§)) = ((1st βπ€) βͺ (2nd
βπ€)) β§ π§πΏπ€)))} |
25 | 1, 24 | eqtr4i 2764 |
. . . 4
β’ π
= {β¨π§, π€β© β£ ((π§ β (On Γ On) β§ π€ β (On Γ On)) β§
(((π₯ β (On Γ On)
β¦ ((1st βπ₯) βͺ (2nd βπ₯)))βπ§) E ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β¨ (((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ§) = ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))βπ€) β§ π§πΏπ€)))} |
26 | | xp1st 7954 |
. . . . . . . 8
β’ (π₯ β (On Γ On) β
(1st βπ₯)
β On) |
27 | | xp2nd 7955 |
. . . . . . . 8
β’ (π₯ β (On Γ On) β
(2nd βπ₯)
β On) |
28 | | fvex 6856 |
. . . . . . . . . 10
β’
(1st βπ₯) β V |
29 | 28 | elon 6327 |
. . . . . . . . 9
β’
((1st βπ₯) β On β Ord (1st
βπ₯)) |
30 | | fvex 6856 |
. . . . . . . . . 10
β’
(2nd βπ₯) β V |
31 | 30 | elon 6327 |
. . . . . . . . 9
β’
((2nd βπ₯) β On β Ord (2nd
βπ₯)) |
32 | | ordun 6422 |
. . . . . . . . 9
β’ ((Ord
(1st βπ₯)
β§ Ord (2nd βπ₯)) β Ord ((1st βπ₯) βͺ (2nd
βπ₯))) |
33 | 29, 31, 32 | syl2anb 599 |
. . . . . . . 8
β’
(((1st βπ₯) β On β§ (2nd
βπ₯) β On) β
Ord ((1st βπ₯) βͺ (2nd βπ₯))) |
34 | 26, 27, 33 | syl2anc 585 |
. . . . . . 7
β’ (π₯ β (On Γ On) β
Ord ((1st βπ₯) βͺ (2nd βπ₯))) |
35 | 28, 30 | unex 7681 |
. . . . . . . 8
β’
((1st βπ₯) βͺ (2nd βπ₯)) β V |
36 | 35 | elon 6327 |
. . . . . . 7
β’
(((1st βπ₯) βͺ (2nd βπ₯)) β On β Ord
((1st βπ₯)
βͺ (2nd βπ₯))) |
37 | 34, 36 | sylibr 233 |
. . . . . 6
β’ (π₯ β (On Γ On) β
((1st βπ₯)
βͺ (2nd βπ₯)) β On) |
38 | 5, 37 | fmpti 7061 |
. . . . 5
β’ (π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))):(On Γ
On)βΆOn |
39 | 38 | a1i 11 |
. . . 4
β’ (β€
β (π₯ β (On
Γ On) β¦ ((1st βπ₯) βͺ (2nd βπ₯))):(On Γ
On)βΆOn) |
40 | | epweon 7710 |
. . . . 5
β’ E We
On |
41 | 40 | a1i 11 |
. . . 4
β’ (β€
β E We On) |
42 | | leweon.1 |
. . . . . 6
β’ πΏ = {β¨π₯, π¦β© β£ ((π₯ β (On Γ On) β§ π¦ β (On Γ On)) β§
((1st βπ₯)
β (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd
βπ₯) β
(2nd βπ¦))))} |
43 | 42 | leweon 9952 |
. . . . 5
β’ πΏ We (On Γ
On) |
44 | 43 | a1i 11 |
. . . 4
β’ (β€
β πΏ We (On Γ
On)) |
45 | | vex 3448 |
. . . . . . . 8
β’ π’ β V |
46 | 45 | dmex 7849 |
. . . . . . 7
β’ dom π’ β V |
47 | 45 | rnex 7850 |
. . . . . . 7
β’ ran π’ β V |
48 | 46, 47 | unex 7681 |
. . . . . 6
β’ (dom
π’ βͺ ran π’) β V |
49 | | imadmres 6187 |
. . . . . . 7
β’ ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β dom ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) βΎ π’)) = ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β π’) |
50 | | inss2 4190 |
. . . . . . . . . 10
β’ (π’ β© (On Γ On)) β
(On Γ On) |
51 | | ssun1 4133 |
. . . . . . . . . . . . . 14
β’ dom π’ β (dom π’ βͺ ran π’) |
52 | | elinel2 4157 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π’ β© (On Γ On)) β π₯ β (On Γ
On)) |
53 | | 1st2nd2 7961 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (On Γ On) β
π₯ = β¨(1st
βπ₯), (2nd
βπ₯)β©) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π’ β© (On Γ On)) β π₯ = β¨(1st
βπ₯), (2nd
βπ₯)β©) |
55 | | elinel1 4156 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π’ β© (On Γ On)) β π₯ β π’) |
56 | 54, 55 | eqeltrrd 2835 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π’ β© (On Γ On)) β
β¨(1st βπ₯), (2nd βπ₯)β© β π’) |
57 | 28, 30 | opeldm 5864 |
. . . . . . . . . . . . . . 15
β’
(β¨(1st βπ₯), (2nd βπ₯)β© β π’ β (1st βπ₯) β dom π’) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π’ β© (On Γ On)) β
(1st βπ₯)
β dom π’) |
59 | 51, 58 | sselid 3943 |
. . . . . . . . . . . . 13
β’ (π₯ β (π’ β© (On Γ On)) β
(1st βπ₯)
β (dom π’ βͺ ran
π’)) |
60 | | ssun2 4134 |
. . . . . . . . . . . . . 14
β’ ran π’ β (dom π’ βͺ ran π’) |
61 | 28, 30 | opelrn 5899 |
. . . . . . . . . . . . . . 15
β’
(β¨(1st βπ₯), (2nd βπ₯)β© β π’ β (2nd βπ₯) β ran π’) |
62 | 56, 61 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π’ β© (On Γ On)) β
(2nd βπ₯)
β ran π’) |
63 | 60, 62 | sselid 3943 |
. . . . . . . . . . . . 13
β’ (π₯ β (π’ β© (On Γ On)) β
(2nd βπ₯)
β (dom π’ βͺ ran
π’)) |
64 | 59, 63 | prssd 4783 |
. . . . . . . . . . . 12
β’ (π₯ β (π’ β© (On Γ On)) β
{(1st βπ₯),
(2nd βπ₯)}
β (dom π’ βͺ ran
π’)) |
65 | 52, 26 | syl 17 |
. . . . . . . . . . . . 13
β’ (π₯ β (π’ β© (On Γ On)) β
(1st βπ₯)
β On) |
66 | 52, 27 | syl 17 |
. . . . . . . . . . . . 13
β’ (π₯ β (π’ β© (On Γ On)) β
(2nd βπ₯)
β On) |
67 | | ordunpr 7762 |
. . . . . . . . . . . . 13
β’
(((1st βπ₯) β On β§ (2nd
βπ₯) β On) β
((1st βπ₯)
βͺ (2nd βπ₯)) β {(1st βπ₯), (2nd βπ₯)}) |
68 | 65, 66, 67 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π₯ β (π’ β© (On Γ On)) β
((1st βπ₯)
βͺ (2nd βπ₯)) β {(1st βπ₯), (2nd βπ₯)}) |
69 | 64, 68 | sseldd 3946 |
. . . . . . . . . . 11
β’ (π₯ β (π’ β© (On Γ On)) β
((1st βπ₯)
βͺ (2nd βπ₯)) β (dom π’ βͺ ran π’)) |
70 | 69 | rgen 3063 |
. . . . . . . . . 10
β’
βπ₯ β
(π’ β© (On Γ
On))((1st βπ₯) βͺ (2nd βπ₯)) β (dom π’ βͺ ran π’) |
71 | | ssrab 4031 |
. . . . . . . . . 10
β’ ((π’ β© (On Γ On)) β
{π₯ β (On Γ On)
β£ ((1st βπ₯) βͺ (2nd βπ₯)) β (dom π’ βͺ ran π’)} β ((π’ β© (On Γ On)) β (On Γ
On) β§ βπ₯ β
(π’ β© (On Γ
On))((1st βπ₯) βͺ (2nd βπ₯)) β (dom π’ βͺ ran π’))) |
72 | 50, 70, 71 | mpbir2an 710 |
. . . . . . . . 9
β’ (π’ β© (On Γ On)) β
{π₯ β (On Γ On)
β£ ((1st βπ₯) βͺ (2nd βπ₯)) β (dom π’ βͺ ran π’)} |
73 | | dmres 5960 |
. . . . . . . . . 10
β’ dom
((π₯ β (On Γ On)
β¦ ((1st βπ₯) βͺ (2nd βπ₯))) βΎ π’) = (π’ β© dom (π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))) |
74 | 38 | fdmi 6681 |
. . . . . . . . . . 11
β’ dom
(π₯ β (On Γ On)
β¦ ((1st βπ₯) βͺ (2nd βπ₯))) = (On Γ
On) |
75 | 74 | ineq2i 4170 |
. . . . . . . . . 10
β’ (π’ β© dom (π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))) = (π’ β© (On Γ On)) |
76 | 73, 75 | eqtri 2761 |
. . . . . . . . 9
β’ dom
((π₯ β (On Γ On)
β¦ ((1st βπ₯) βͺ (2nd βπ₯))) βΎ π’) = (π’ β© (On Γ On)) |
77 | 5 | mptpreima 6191 |
. . . . . . . . 9
β’ (β‘(π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β (dom π’ βͺ ran π’)) = {π₯ β (On Γ On) β£
((1st βπ₯)
βͺ (2nd βπ₯)) β (dom π’ βͺ ran π’)} |
78 | 72, 76, 77 | 3sstr4i 3988 |
. . . . . . . 8
β’ dom
((π₯ β (On Γ On)
β¦ ((1st βπ₯) βͺ (2nd βπ₯))) βΎ π’) β (β‘(π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β (dom π’ βͺ ran π’)) |
79 | | funmpt 6540 |
. . . . . . . . 9
β’ Fun
(π₯ β (On Γ On)
β¦ ((1st βπ₯) βͺ (2nd βπ₯))) |
80 | | resss 5963 |
. . . . . . . . . 10
β’ ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) βΎ π’) β (π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) |
81 | | dmss 5859 |
. . . . . . . . . 10
β’ (((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) βΎ π’) β (π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β dom ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) βΎ π’) β dom (π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))) |
82 | 80, 81 | ax-mp 5 |
. . . . . . . . 9
β’ dom
((π₯ β (On Γ On)
β¦ ((1st βπ₯) βͺ (2nd βπ₯))) βΎ π’) β dom (π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) |
83 | | funimass3 7005 |
. . . . . . . . 9
β’ ((Fun
(π₯ β (On Γ On)
β¦ ((1st βπ₯) βͺ (2nd βπ₯))) β§ dom ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) βΎ π’) β dom (π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯)))) β (((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β dom ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) βΎ π’)) β (dom π’ βͺ ran π’) β dom ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) βΎ π’) β (β‘(π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β (dom π’ βͺ ran π’)))) |
84 | 79, 82, 83 | mp2an 691 |
. . . . . . . 8
β’ (((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β dom ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) βΎ π’)) β (dom π’ βͺ ran π’) β dom ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) βΎ π’) β (β‘(π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β (dom π’ βͺ ran π’))) |
85 | 78, 84 | mpbir 230 |
. . . . . . 7
β’ ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β dom ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) βΎ π’)) β (dom π’ βͺ ran π’) |
86 | 49, 85 | eqsstrri 3980 |
. . . . . 6
β’ ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β π’) β (dom π’ βͺ ran π’) |
87 | 48, 86 | ssexi 5280 |
. . . . 5
β’ ((π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β π’) β V |
88 | 87 | a1i 11 |
. . . 4
β’ (β€
β ((π₯ β (On
Γ On) β¦ ((1st βπ₯) βͺ (2nd βπ₯))) β π’) β V) |
89 | 25, 39, 41, 44, 88 | fnwe 8065 |
. . 3
β’ (β€
β π
We (On Γ
On)) |
90 | | epse 5617 |
. . . . 5
β’ E Se
On |
91 | 90 | a1i 11 |
. . . 4
β’ (β€
β E Se On) |
92 | | vuniex 7677 |
. . . . . . . 8
β’ βͺ π’
β V |
93 | 92 | pwex 5336 |
. . . . . . 7
β’ π«
βͺ π’ β V |
94 | 93, 93 | xpex 7688 |
. . . . . 6
β’
(π« βͺ π’ Γ π« βͺ π’)
β V |
95 | 5 | mptpreima 6191 |
. . . . . . . 8
β’ (β‘(π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β π’) = {π₯ β (On Γ On) β£
((1st βπ₯)
βͺ (2nd βπ₯)) β π’} |
96 | | df-rab 3407 |
. . . . . . . 8
β’ {π₯ β (On Γ On) β£
((1st βπ₯)
βͺ (2nd βπ₯)) β π’} = {π₯ β£ (π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’)} |
97 | 95, 96 | eqtri 2761 |
. . . . . . 7
β’ (β‘(π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β π’) = {π₯ β£ (π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’)} |
98 | 53 | adantr 482 |
. . . . . . . . 9
β’ ((π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
99 | | elssuni 4899 |
. . . . . . . . . . . . 13
β’
(((1st βπ₯) βͺ (2nd βπ₯)) β π’ β ((1st βπ₯) βͺ (2nd
βπ₯)) β βͺ π’) |
100 | 99 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’) β ((1st βπ₯) βͺ (2nd
βπ₯)) β βͺ π’) |
101 | 100 | unssad 4148 |
. . . . . . . . . . 11
β’ ((π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’) β (1st βπ₯) β βͺ π’) |
102 | 28 | elpw 4565 |
. . . . . . . . . . 11
β’
((1st βπ₯) β π« βͺ π’
β (1st βπ₯) β βͺ π’) |
103 | 101, 102 | sylibr 233 |
. . . . . . . . . 10
β’ ((π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’) β (1st βπ₯) β π« βͺ π’) |
104 | 100 | unssbd 4149 |
. . . . . . . . . . 11
β’ ((π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’) β (2nd βπ₯) β βͺ π’) |
105 | 30 | elpw 4565 |
. . . . . . . . . . 11
β’
((2nd βπ₯) β π« βͺ π’
β (2nd βπ₯) β βͺ π’) |
106 | 104, 105 | sylibr 233 |
. . . . . . . . . 10
β’ ((π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’) β (2nd βπ₯) β π« βͺ π’) |
107 | 103, 106 | jca 513 |
. . . . . . . . 9
β’ ((π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’) β ((1st βπ₯) β π« βͺ π’
β§ (2nd βπ₯) β π« βͺ π’)) |
108 | | elxp6 7956 |
. . . . . . . . 9
β’ (π₯ β (π« βͺ π’
Γ π« βͺ π’) β (π₯ = β¨(1st βπ₯), (2nd βπ₯)β© β§ ((1st
βπ₯) β π«
βͺ π’ β§ (2nd βπ₯) β π« βͺ π’))) |
109 | 98, 107, 108 | sylanbrc 584 |
. . . . . . . 8
β’ ((π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’) β π₯ β (π« βͺ π’
Γ π« βͺ π’)) |
110 | 109 | abssi 4028 |
. . . . . . 7
β’ {π₯ β£ (π₯ β (On Γ On) β§
((1st βπ₯)
βͺ (2nd βπ₯)) β π’)} β (π« βͺ π’
Γ π« βͺ π’) |
111 | 97, 110 | eqsstri 3979 |
. . . . . 6
β’ (β‘(π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β π’) β (π« βͺ π’
Γ π« βͺ π’) |
112 | 94, 111 | ssexi 5280 |
. . . . 5
β’ (β‘(π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β π’) β V |
113 | 112 | a1i 11 |
. . . 4
β’ (β€
β (β‘(π₯ β (On Γ On) β¦
((1st βπ₯)
βͺ (2nd βπ₯))) β π’) β V) |
114 | 25, 39, 91, 113 | fnse 8066 |
. . 3
β’ (β€
β π
Se (On Γ
On)) |
115 | 89, 114 | jca 513 |
. 2
β’ (β€
β (π
We (On Γ
On) β§ π
Se (On Γ
On))) |
116 | 115 | mptru 1549 |
1
β’ (π
We (On Γ On) β§ π
Se (On Γ
On)) |