Step | Hyp | Ref
| Expression |
1 | | naddunif.1 |
. . 3
β’ (π β π΄ β On) |
2 | | naddunif.2 |
. . 3
β’ (π β π΅ β On) |
3 | | naddov3 8627 |
. . 3
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) = β© {π€ β On β£ (( +no
β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅}))) β π€}) |
4 | 1, 2, 3 | syl2anc 585 |
. 2
β’ (π β (π΄ +no π΅) = β© {π€ β On β£ (( +no
β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅}))) β π€}) |
5 | | naddfn 8622 |
. . . . . . 7
β’ +no Fn
(On Γ On) |
6 | | fnfun 6603 |
. . . . . . 7
β’ ( +no Fn
(On Γ On) β Fun +no ) |
7 | 5, 6 | ax-mp 5 |
. . . . . 6
β’ Fun
+no |
8 | | snex 5389 |
. . . . . . 7
β’ {π΄} β V |
9 | | xpexg 7685 |
. . . . . . 7
β’ (({π΄} β V β§ π΅ β On) β ({π΄} Γ π΅) β V) |
10 | 8, 2, 9 | sylancr 588 |
. . . . . 6
β’ (π β ({π΄} Γ π΅) β V) |
11 | | funimaexg 6588 |
. . . . . 6
β’ ((Fun +no
β§ ({π΄} Γ π΅) β V) β ( +no β
({π΄} Γ π΅)) β V) |
12 | 7, 10, 11 | sylancr 588 |
. . . . 5
β’ (π β ( +no β ({π΄} Γ π΅)) β V) |
13 | | imassrn 6025 |
. . . . . . 7
β’ ( +no
β ({π΄} Γ π΅)) β ran
+no |
14 | | naddf 8628 |
. . . . . . . 8
β’ +no :(On
Γ On)βΆOn |
15 | | frn 6676 |
. . . . . . . 8
β’ ( +no
:(On Γ On)βΆOn β ran +no β On) |
16 | 14, 15 | ax-mp 5 |
. . . . . . 7
β’ ran +no
β On |
17 | 13, 16 | sstri 3954 |
. . . . . 6
β’ ( +no
β ({π΄} Γ π΅)) β On |
18 | 17 | a1i 11 |
. . . . 5
β’ (π β ( +no β ({π΄} Γ π΅)) β On) |
19 | 12, 18 | elpwd 4567 |
. . . 4
β’ (π β ( +no β ({π΄} Γ π΅)) β π« On) |
20 | | snex 5389 |
. . . . . . 7
β’ {π΅} β V |
21 | | xpexg 7685 |
. . . . . . 7
β’ ((π΄ β On β§ {π΅} β V) β (π΄ Γ {π΅}) β V) |
22 | 1, 20, 21 | sylancl 587 |
. . . . . 6
β’ (π β (π΄ Γ {π΅}) β V) |
23 | | funimaexg 6588 |
. . . . . 6
β’ ((Fun +no
β§ (π΄ Γ {π΅}) β V) β ( +no
β (π΄ Γ {π΅})) β V) |
24 | 7, 22, 23 | sylancr 588 |
. . . . 5
β’ (π β ( +no β (π΄ Γ {π΅})) β V) |
25 | | imassrn 6025 |
. . . . . . 7
β’ ( +no
β (π΄ Γ {π΅})) β ran
+no |
26 | 25, 16 | sstri 3954 |
. . . . . 6
β’ ( +no
β (π΄ Γ {π΅})) β On |
27 | 26 | a1i 11 |
. . . . 5
β’ (π β ( +no β (π΄ Γ {π΅})) β On) |
28 | 24, 27 | elpwd 4567 |
. . . 4
β’ (π β ( +no β (π΄ Γ {π΅})) β π« On) |
29 | | pwuncl 7705 |
. . . 4
β’ ((( +no
β ({π΄} Γ π΅)) β π« On β§ (
+no β (π΄ Γ
{π΅})) β π« On)
β (( +no β ({π΄}
Γ π΅)) βͺ ( +no
β (π΄ Γ {π΅}))) β π«
On) |
30 | 19, 28, 29 | syl2anc 585 |
. . 3
β’ (π β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅}))) β π« On) |
31 | | naddunif.3 |
. . . . . . . . . 10
β’ (π β π΄ = β© {π₯ β On β£ π β π₯}) |
32 | 31, 1 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (π β β© {π₯
β On β£ π β
π₯} β
On) |
33 | | onintrab2 7733 |
. . . . . . . . 9
β’
(βπ₯ β On
π β π₯ β β© {π₯
β On β£ π β
π₯} β
On) |
34 | 32, 33 | sylibr 233 |
. . . . . . . 8
β’ (π β βπ₯ β On π β π₯) |
35 | | vex 3450 |
. . . . . . . . . 10
β’ π₯ β V |
36 | 35 | ssex 5279 |
. . . . . . . . 9
β’ (π β π₯ β π β V) |
37 | 36 | rexlimivw 3149 |
. . . . . . . 8
β’
(βπ₯ β On
π β π₯ β π β V) |
38 | 34, 37 | syl 17 |
. . . . . . 7
β’ (π β π β V) |
39 | | xpexg 7685 |
. . . . . . 7
β’ ((π β V β§ {π΅} β V) β (π Γ {π΅}) β V) |
40 | 38, 20, 39 | sylancl 587 |
. . . . . 6
β’ (π β (π Γ {π΅}) β V) |
41 | | funimaexg 6588 |
. . . . . 6
β’ ((Fun +no
β§ (π Γ {π΅}) β V) β ( +no
β (π Γ {π΅})) β V) |
42 | 7, 40, 41 | sylancr 588 |
. . . . 5
β’ (π β ( +no β (π Γ {π΅})) β V) |
43 | | imassrn 6025 |
. . . . . . 7
β’ ( +no
β (π Γ {π΅})) β ran
+no |
44 | 43, 16 | sstri 3954 |
. . . . . 6
β’ ( +no
β (π Γ {π΅})) β On |
45 | 44 | a1i 11 |
. . . . 5
β’ (π β ( +no β (π Γ {π΅})) β On) |
46 | 42, 45 | elpwd 4567 |
. . . 4
β’ (π β ( +no β (π Γ {π΅})) β π« On) |
47 | | naddunif.4 |
. . . . . . . . . 10
β’ (π β π΅ = β© {π¦ β On β£ π β π¦}) |
48 | 47, 2 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (π β β© {π¦
β On β£ π β
π¦} β
On) |
49 | | onintrab2 7733 |
. . . . . . . . 9
β’
(βπ¦ β On
π β π¦ β β© {π¦
β On β£ π β
π¦} β
On) |
50 | 48, 49 | sylibr 233 |
. . . . . . . 8
β’ (π β βπ¦ β On π β π¦) |
51 | | vex 3450 |
. . . . . . . . . 10
β’ π¦ β V |
52 | 51 | ssex 5279 |
. . . . . . . . 9
β’ (π β π¦ β π β V) |
53 | 52 | rexlimivw 3149 |
. . . . . . . 8
β’
(βπ¦ β On
π β π¦ β π β V) |
54 | 50, 53 | syl 17 |
. . . . . . 7
β’ (π β π β V) |
55 | | xpexg 7685 |
. . . . . . 7
β’ (({π΄} β V β§ π β V) β ({π΄} Γ π) β V) |
56 | 8, 54, 55 | sylancr 588 |
. . . . . 6
β’ (π β ({π΄} Γ π) β V) |
57 | | funimaexg 6588 |
. . . . . 6
β’ ((Fun +no
β§ ({π΄} Γ π) β V) β ( +no β
({π΄} Γ π)) β V) |
58 | 7, 56, 57 | sylancr 588 |
. . . . 5
β’ (π β ( +no β ({π΄} Γ π)) β V) |
59 | | imassrn 6025 |
. . . . . . 7
β’ ( +no
β ({π΄} Γ π)) β ran
+no |
60 | 59, 16 | sstri 3954 |
. . . . . 6
β’ ( +no
β ({π΄} Γ π)) β On |
61 | 60 | a1i 11 |
. . . . 5
β’ (π β ( +no β ({π΄} Γ π)) β On) |
62 | 58, 61 | elpwd 4567 |
. . . 4
β’ (π β ( +no β ({π΄} Γ π)) β π« On) |
63 | | pwuncl 7705 |
. . . 4
β’ ((( +no
β (π Γ {π΅})) β π« On β§ (
+no β ({π΄} Γ
π)) β π« On)
β (( +no β (π
Γ {π΅})) βͺ ( +no
β ({π΄} Γ π))) β π«
On) |
64 | 46, 62, 63 | syl2anc 585 |
. . 3
β’ (π β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π))) β π« On) |
65 | 2, 47 | cofonr 8621 |
. . . . . . . . 9
β’ (π β βπ β π΅ βπ β π π β π ) |
66 | | onss 7720 |
. . . . . . . . . . . . . . 15
β’ (π΅ β On β π΅ β On) |
67 | 2, 66 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β On) |
68 | 67 | sselda 3945 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β π β On) |
69 | 68 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ π β π) β π β On) |
70 | | onss 7720 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β On β π¦ β On) |
71 | 70 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β On) β π¦ β On) |
72 | | sstr 3953 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π¦ β§ π¦ β On) β π β On) |
73 | 72 | expcom 415 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β On β (π β π¦ β π β On)) |
74 | 71, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β On) β (π β π¦ β π β On)) |
75 | 74 | rexlimdva 3153 |
. . . . . . . . . . . . . . 15
β’ (π β (βπ¦ β On π β π¦ β π β On)) |
76 | 50, 75 | mpd 15 |
. . . . . . . . . . . . . 14
β’ (π β π β On) |
77 | 76 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β π β On) |
78 | 77 | sselda 3945 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ π β π) β π β On) |
79 | 1 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ π β π) β π΄ β On) |
80 | | naddss2 8636 |
. . . . . . . . . . . 12
β’ ((π β On β§ π β On β§ π΄ β On) β (π β π β (π΄ +no π) β (π΄ +no π ))) |
81 | 69, 78, 79, 80 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π β π΅) β§ π β π) β (π β π β (π΄ +no π) β (π΄ +no π ))) |
82 | 81 | rexbidva 3174 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β (βπ β π π β π β βπ β π (π΄ +no π) β (π΄ +no π ))) |
83 | 82 | ralbidva 3173 |
. . . . . . . . 9
β’ (π β (βπ β π΅ βπ β π π β π β βπ β π΅ βπ β π (π΄ +no π) β (π΄ +no π ))) |
84 | 65, 83 | mpbid 231 |
. . . . . . . 8
β’ (π β βπ β π΅ βπ β π (π΄ +no π) β (π΄ +no π )) |
85 | 1 | snssd 4770 |
. . . . . . . . . . . 12
β’ (π β {π΄} β On) |
86 | | xpss12 5649 |
. . . . . . . . . . . 12
β’ (({π΄} β On β§ π β On) β ({π΄} Γ π) β (On Γ On)) |
87 | 85, 76, 86 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ({π΄} Γ π) β (On Γ On)) |
88 | | sseq2 3971 |
. . . . . . . . . . . 12
β’ (π = (π +no π ) β ((π΄ +no π) β π β (π΄ +no π) β (π +no π ))) |
89 | 88 | imaeqexov 7593 |
. . . . . . . . . . 11
β’ (( +no Fn
(On Γ On) β§ ({π΄}
Γ π) β (On
Γ On)) β (βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π β βπ β {π΄}βπ β π (π΄ +no π) β (π +no π ))) |
90 | 5, 87, 89 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π β βπ β {π΄}βπ β π (π΄ +no π) β (π +no π ))) |
91 | | oveq1 7365 |
. . . . . . . . . . . . . 14
β’ (π = π΄ β (π +no π ) = (π΄ +no π )) |
92 | 91 | sseq2d 3977 |
. . . . . . . . . . . . 13
β’ (π = π΄ β ((π΄ +no π) β (π +no π ) β (π΄ +no π) β (π΄ +no π ))) |
93 | 92 | rexbidv 3176 |
. . . . . . . . . . . 12
β’ (π = π΄ β (βπ β π (π΄ +no π) β (π +no π ) β βπ β π (π΄ +no π) β (π΄ +no π ))) |
94 | 93 | rexsng 4636 |
. . . . . . . . . . 11
β’ (π΄ β On β (βπ β {π΄}βπ β π (π΄ +no π) β (π +no π ) β βπ β π (π΄ +no π) β (π΄ +no π ))) |
95 | 1, 94 | syl 17 |
. . . . . . . . . 10
β’ (π β (βπ β {π΄}βπ β π (π΄ +no π) β (π +no π ) β βπ β π (π΄ +no π) β (π΄ +no π ))) |
96 | 90, 95 | bitrd 279 |
. . . . . . . . 9
β’ (π β (βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π β βπ β π (π΄ +no π) β (π΄ +no π ))) |
97 | 96 | ralbidv 3175 |
. . . . . . . 8
β’ (π β (βπ β π΅ βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π β βπ β π΅ βπ β π (π΄ +no π) β (π΄ +no π ))) |
98 | 84, 97 | mpbird 257 |
. . . . . . 7
β’ (π β βπ β π΅ βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π) |
99 | | olc 867 |
. . . . . . . 8
β’
(βπ β (
+no β ({π΄} Γ
π))(π΄ +no π) β π β (βπ β ( +no β (π Γ {π΅}))(π΄ +no π) β π β¨ βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π)) |
100 | 99 | ralimi 3087 |
. . . . . . 7
β’
(βπ β
π΅ βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π β βπ β π΅ (βπ β ( +no β (π Γ {π΅}))(π΄ +no π) β π β¨ βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π)) |
101 | 98, 100 | syl 17 |
. . . . . 6
β’ (π β βπ β π΅ (βπ β ( +no β (π Γ {π΅}))(π΄ +no π) β π β¨ βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π)) |
102 | | rexun 4151 |
. . . . . . 7
β’
(βπ β ((
+no β (π Γ
{π΅})) βͺ ( +no β
({π΄} Γ π)))(π΄ +no π) β π β (βπ β ( +no β (π Γ {π΅}))(π΄ +no π) β π β¨ βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π)) |
103 | 102 | ralbii 3097 |
. . . . . 6
β’
(βπ β
π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π΄ +no π) β π β βπ β π΅ (βπ β ( +no β (π Γ {π΅}))(π΄ +no π) β π β¨ βπ β ( +no β ({π΄} Γ π))(π΄ +no π) β π)) |
104 | 101, 103 | sylibr 233 |
. . . . 5
β’ (π β βπ β π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π΄ +no π) β π) |
105 | | xpss12 5649 |
. . . . . . . 8
β’ (({π΄} β On β§ π΅ β On) β ({π΄} Γ π΅) β (On Γ On)) |
106 | 85, 67, 105 | syl2anc 585 |
. . . . . . 7
β’ (π β ({π΄} Γ π΅) β (On Γ On)) |
107 | | sseq1 3970 |
. . . . . . . . 9
β’ (π = (π +no π) β (π β π β (π +no π) β π)) |
108 | 107 | rexbidv 3176 |
. . . . . . . 8
β’ (π = (π +no π) β (βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π β βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π)) |
109 | 108 | imaeqalov 7594 |
. . . . . . 7
β’ (( +no Fn
(On Γ On) β§ ({π΄}
Γ π΅) β (On
Γ On)) β (βπ β ( +no β ({π΄} Γ π΅))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π β βπ β {π΄}βπ β π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π)) |
110 | 5, 106, 109 | sylancr 588 |
. . . . . 6
β’ (π β (βπ β ( +no β ({π΄} Γ π΅))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π β βπ β {π΄}βπ β π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π)) |
111 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π = π΄ β (π +no π) = (π΄ +no π)) |
112 | 111 | sseq1d 3976 |
. . . . . . . . . 10
β’ (π = π΄ β ((π +no π) β π β (π΄ +no π) β π)) |
113 | 112 | rexbidv 3176 |
. . . . . . . . 9
β’ (π = π΄ β (βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π β βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π΄ +no π) β π)) |
114 | 113 | ralbidv 3175 |
. . . . . . . 8
β’ (π = π΄ β (βπ β π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π β βπ β π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π΄ +no π) β π)) |
115 | 114 | ralsng 4635 |
. . . . . . 7
β’ (π΄ β On β (βπ β {π΄}βπ β π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π β βπ β π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π΄ +no π) β π)) |
116 | 1, 115 | syl 17 |
. . . . . 6
β’ (π β (βπ β {π΄}βπ β π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π β βπ β π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π΄ +no π) β π)) |
117 | 110, 116 | bitrd 279 |
. . . . 5
β’ (π β (βπ β ( +no β ({π΄} Γ π΅))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π β βπ β π΅ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π΄ +no π) β π)) |
118 | 104, 117 | mpbird 257 |
. . . 4
β’ (π β βπ β ( +no β ({π΄} Γ π΅))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π) |
119 | 1, 31 | cofonr 8621 |
. . . . . . . . . 10
β’ (π β βπ β π΄ βπ β π π β π) |
120 | | onss 7720 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β On β π΄ β On) |
121 | 1, 120 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β On) |
122 | 121 | sselda 3945 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π β On) |
123 | 122 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β π) β π β On) |
124 | | ssintub 4928 |
. . . . . . . . . . . . . . . 16
β’ π β β© {π₯
β On β£ π β
π₯} |
125 | 31, 121 | eqsstrrd 3984 |
. . . . . . . . . . . . . . . 16
β’ (π β β© {π₯
β On β£ π β
π₯} β
On) |
126 | 124, 125 | sstrid 3956 |
. . . . . . . . . . . . . . 15
β’ (π β π β On) |
127 | 126 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π β On) |
128 | 127 | sselda 3945 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β π) β π β On) |
129 | 2 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ π β π) β π΅ β On) |
130 | | naddss1 8635 |
. . . . . . . . . . . . 13
β’ ((π β On β§ π β On β§ π΅ β On) β (π β π β (π +no π΅) β (π +no π΅))) |
131 | 123, 128,
129, 130 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ π β π) β (π β π β (π +no π΅) β (π +no π΅))) |
132 | 131 | rexbidva 3174 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (βπ β π π β π β βπ β π (π +no π΅) β (π +no π΅))) |
133 | 132 | ralbidva 3173 |
. . . . . . . . . 10
β’ (π β (βπ β π΄ βπ β π π β π β βπ β π΄ βπ β π (π +no π΅) β (π +no π΅))) |
134 | 119, 133 | mpbid 231 |
. . . . . . . . 9
β’ (π β βπ β π΄ βπ β π (π +no π΅) β (π +no π΅)) |
135 | 2 | snssd 4770 |
. . . . . . . . . . . . 13
β’ (π β {π΅} β On) |
136 | | xpss12 5649 |
. . . . . . . . . . . . 13
β’ ((π β On β§ {π΅} β On) β (π Γ {π΅}) β (On Γ On)) |
137 | 126, 135,
136 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (π Γ {π΅}) β (On Γ On)) |
138 | | sseq2 3971 |
. . . . . . . . . . . . 13
β’ (π = (π +no π ) β ((π +no π΅) β π β (π +no π΅) β (π +no π ))) |
139 | 138 | imaeqexov 7593 |
. . . . . . . . . . . 12
β’ (( +no Fn
(On Γ On) β§ (π
Γ {π΅}) β (On
Γ On)) β (βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π β βπ β π βπ β {π΅} (π +no π΅) β (π +no π ))) |
140 | 5, 137, 139 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β (βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π β βπ β π βπ β {π΅} (π +no π΅) β (π +no π ))) |
141 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
β’ (π = π΅ β (π +no π ) = (π +no π΅)) |
142 | 141 | sseq2d 3977 |
. . . . . . . . . . . . . 14
β’ (π = π΅ β ((π +no π΅) β (π +no π ) β (π +no π΅) β (π +no π΅))) |
143 | 142 | rexsng 4636 |
. . . . . . . . . . . . 13
β’ (π΅ β On β (βπ β {π΅} (π +no π΅) β (π +no π ) β (π +no π΅) β (π +no π΅))) |
144 | 2, 143 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (βπ β {π΅} (π +no π΅) β (π +no π ) β (π +no π΅) β (π +no π΅))) |
145 | 144 | rexbidv 3176 |
. . . . . . . . . . 11
β’ (π β (βπ β π βπ β {π΅} (π +no π΅) β (π +no π ) β βπ β π (π +no π΅) β (π +no π΅))) |
146 | 140, 145 | bitrd 279 |
. . . . . . . . . 10
β’ (π β (βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π β βπ β π (π +no π΅) β (π +no π΅))) |
147 | 146 | ralbidv 3175 |
. . . . . . . . 9
β’ (π β (βπ β π΄ βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π β βπ β π΄ βπ β π (π +no π΅) β (π +no π΅))) |
148 | 134, 147 | mpbird 257 |
. . . . . . . 8
β’ (π β βπ β π΄ βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π) |
149 | | orc 866 |
. . . . . . . . 9
β’
(βπ β (
+no β (π Γ
{π΅}))(π +no π΅) β π β (βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π β¨ βπ β ( +no β ({π΄} Γ π))(π +no π΅) β π)) |
150 | 149 | ralimi 3087 |
. . . . . . . 8
β’
(βπ β
π΄ βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π β βπ β π΄ (βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π β¨ βπ β ( +no β ({π΄} Γ π))(π +no π΅) β π)) |
151 | 148, 150 | syl 17 |
. . . . . . 7
β’ (π β βπ β π΄ (βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π β¨ βπ β ( +no β ({π΄} Γ π))(π +no π΅) β π)) |
152 | | rexun 4151 |
. . . . . . . 8
β’
(βπ β ((
+no β (π Γ
{π΅})) βͺ ( +no β
({π΄} Γ π)))(π +no π΅) β π β (βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π β¨ βπ β ( +no β ({π΄} Γ π))(π +no π΅) β π)) |
153 | 152 | ralbii 3097 |
. . . . . . 7
β’
(βπ β
π΄ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π΅) β π β βπ β π΄ (βπ β ( +no β (π Γ {π΅}))(π +no π΅) β π β¨ βπ β ( +no β ({π΄} Γ π))(π +no π΅) β π)) |
154 | 151, 153 | sylibr 233 |
. . . . . 6
β’ (π β βπ β π΄ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π΅) β π) |
155 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π = π΅ β (π +no π) = (π +no π΅)) |
156 | 155 | sseq1d 3976 |
. . . . . . . . . 10
β’ (π = π΅ β ((π +no π) β π β (π +no π΅) β π)) |
157 | 156 | rexbidv 3176 |
. . . . . . . . 9
β’ (π = π΅ β (βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π β βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π΅) β π)) |
158 | 157 | ralsng 4635 |
. . . . . . . 8
β’ (π΅ β On β (βπ β {π΅}βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π β βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π΅) β π)) |
159 | 2, 158 | syl 17 |
. . . . . . 7
β’ (π β (βπ β {π΅}βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π β βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π΅) β π)) |
160 | 159 | ralbidv 3175 |
. . . . . 6
β’ (π β (βπ β π΄ βπ β {π΅}βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π β βπ β π΄ βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π΅) β π)) |
161 | 154, 160 | mpbird 257 |
. . . . 5
β’ (π β βπ β π΄ βπ β {π΅}βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π) |
162 | | xpss12 5649 |
. . . . . . 7
β’ ((π΄ β On β§ {π΅} β On) β (π΄ Γ {π΅}) β (On Γ On)) |
163 | 121, 135,
162 | syl2anc 585 |
. . . . . 6
β’ (π β (π΄ Γ {π΅}) β (On Γ On)) |
164 | 108 | imaeqalov 7594 |
. . . . . 6
β’ (( +no Fn
(On Γ On) β§ (π΄
Γ {π΅}) β (On
Γ On)) β (βπ β ( +no β (π΄ Γ {π΅}))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π β βπ β π΄ βπ β {π΅}βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π)) |
165 | 5, 163, 164 | sylancr 588 |
. . . . 5
β’ (π β (βπ β ( +no β (π΄ Γ {π΅}))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π β βπ β π΄ βπ β {π΅}βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))(π +no π) β π)) |
166 | 161, 165 | mpbird 257 |
. . . 4
β’ (π β βπ β ( +no β (π΄ Γ {π΅}))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π) |
167 | | ralunb 4152 |
. . . 4
β’
(βπ β ((
+no β ({π΄} Γ
π΅)) βͺ ( +no β
(π΄ Γ {π΅})))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π β (βπ β ( +no β ({π΄} Γ π΅))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π β§ βπ β ( +no β (π΄ Γ {π΅}))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π)) |
168 | 118, 166,
167 | sylanbrc 584 |
. . 3
β’ (π β βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))π β π) |
169 | 124, 31 | sseqtrrid 3998 |
. . . . . . . . . . . 12
β’ (π β π β π΄) |
170 | 169 | sselda 3945 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β π β π΄) |
171 | | ssid 3967 |
. . . . . . . . . . 11
β’ π β π |
172 | | sseq2 3971 |
. . . . . . . . . . . 12
β’ (π = π β (π β π β π β π)) |
173 | 172 | rspcev 3582 |
. . . . . . . . . . 11
β’ ((π β π΄ β§ π β π) β βπ β π΄ π β π) |
174 | 170, 171,
173 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β§ π β π) β βπ β π΄ π β π) |
175 | 174 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ β π βπ β π΄ π β π) |
176 | 126 | sselda 3945 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β On) |
177 | 176 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β π΄) β π β On) |
178 | 121 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π΄ β On) |
179 | 178 | sselda 3945 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β π΄) β π β On) |
180 | 2 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β π΄) β π΅ β On) |
181 | 177, 179,
180, 130 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β π΄) β (π β π β (π +no π΅) β (π +no π΅))) |
182 | 181 | rexbidva 3174 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (βπ β π΄ π β π β βπ β π΄ (π +no π΅) β (π +no π΅))) |
183 | 182 | ralbidva 3173 |
. . . . . . . . 9
β’ (π β (βπ β π βπ β π΄ π β π β βπ β π βπ β π΄ (π +no π΅) β (π +no π΅))) |
184 | 175, 183 | mpbid 231 |
. . . . . . . 8
β’ (π β βπ β π βπ β π΄ (π +no π΅) β (π +no π΅)) |
185 | | sseq2 3971 |
. . . . . . . . . . . 12
β’ (π = (π +no π ) β ((π +no π΅) β π β (π +no π΅) β (π +no π ))) |
186 | 185 | imaeqexov 7593 |
. . . . . . . . . . 11
β’ (( +no Fn
(On Γ On) β§ (π΄
Γ {π΅}) β (On
Γ On)) β (βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π β βπ β π΄ βπ β {π΅} (π +no π΅) β (π +no π ))) |
187 | 5, 163, 186 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π β βπ β π΄ βπ β {π΅} (π +no π΅) β (π +no π ))) |
188 | 144 | rexbidv 3176 |
. . . . . . . . . 10
β’ (π β (βπ β π΄ βπ β {π΅} (π +no π΅) β (π +no π ) β βπ β π΄ (π +no π΅) β (π +no π΅))) |
189 | 187, 188 | bitrd 279 |
. . . . . . . . 9
β’ (π β (βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π β βπ β π΄ (π +no π΅) β (π +no π΅))) |
190 | 189 | ralbidv 3175 |
. . . . . . . 8
β’ (π β (βπ β π βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π β βπ β π βπ β π΄ (π +no π΅) β (π +no π΅))) |
191 | 184, 190 | mpbird 257 |
. . . . . . 7
β’ (π β βπ β π βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π) |
192 | | olc 867 |
. . . . . . . 8
β’
(βπ β (
+no β (π΄ Γ
{π΅}))(π +no π΅) β π β (βπ β ( +no β ({π΄} Γ π΅))(π +no π΅) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π)) |
193 | 192 | ralimi 3087 |
. . . . . . 7
β’
(βπ β
π βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π β βπ β π (βπ β ( +no β ({π΄} Γ π΅))(π +no π΅) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π)) |
194 | 191, 193 | syl 17 |
. . . . . 6
β’ (π β βπ β π (βπ β ( +no β ({π΄} Γ π΅))(π +no π΅) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π)) |
195 | 155 | sseq1d 3976 |
. . . . . . . . . . . 12
β’ (π = π΅ β ((π +no π) β π β (π +no π΅) β π)) |
196 | 195 | rexbidv 3176 |
. . . . . . . . . . 11
β’ (π = π΅ β (βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π β βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π΅) β π)) |
197 | 196 | ralsng 4635 |
. . . . . . . . . 10
β’ (π΅ β On β (βπ β {π΅}βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π β βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π΅) β π)) |
198 | 2, 197 | syl 17 |
. . . . . . . . 9
β’ (π β (βπ β {π΅}βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π β βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π΅) β π)) |
199 | 198 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β (βπ β {π΅}βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π β βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π΅) β π)) |
200 | | rexun 4151 |
. . . . . . . 8
β’
(βπ β ((
+no β ({π΄} Γ
π΅)) βͺ ( +no β
(π΄ Γ {π΅})))(π +no π΅) β π β (βπ β ( +no β ({π΄} Γ π΅))(π +no π΅) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π)) |
201 | 199, 200 | bitrdi 287 |
. . . . . . 7
β’ ((π β§ π β π) β (βπ β {π΅}βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π β (βπ β ( +no β ({π΄} Γ π΅))(π +no π΅) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π))) |
202 | 201 | ralbidva 3173 |
. . . . . 6
β’ (π β (βπ β π βπ β {π΅}βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π β βπ β π (βπ β ( +no β ({π΄} Γ π΅))(π +no π΅) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π +no π΅) β π))) |
203 | 194, 202 | mpbird 257 |
. . . . 5
β’ (π β βπ β π βπ β {π΅}βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π) |
204 | | sseq1 3970 |
. . . . . . . 8
β’ (π = (π +no π) β (π β π β (π +no π) β π)) |
205 | 204 | rexbidv 3176 |
. . . . . . 7
β’ (π = (π +no π) β (βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π β βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π)) |
206 | 205 | imaeqalov 7594 |
. . . . . 6
β’ (( +no Fn
(On Γ On) β§ (π
Γ {π΅}) β (On
Γ On)) β (βπ β ( +no β (π Γ {π΅}))βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π β βπ β π βπ β {π΅}βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π)) |
207 | 5, 137, 206 | sylancr 588 |
. . . . 5
β’ (π β (βπ β ( +no β (π Γ {π΅}))βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π β βπ β π βπ β {π΅}βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π)) |
208 | 203, 207 | mpbird 257 |
. . . 4
β’ (π β βπ β ( +no β (π Γ {π΅}))βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π) |
209 | | ssintub 4928 |
. . . . . . . . . . . . 13
β’ π β β© {π¦
β On β£ π β
π¦} |
210 | 209, 47 | sseqtrrid 3998 |
. . . . . . . . . . . 12
β’ (π β π β π΅) |
211 | 210 | sselda 3945 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β π β π΅) |
212 | | ssid 3967 |
. . . . . . . . . . 11
β’ π β π |
213 | | sseq2 3971 |
. . . . . . . . . . . 12
β’ (π = π β (π β π β π β π)) |
214 | 213 | rspcev 3582 |
. . . . . . . . . . 11
β’ ((π β π΅ β§ π β π) β βπ β π΅ π β π ) |
215 | 211, 212,
214 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β§ π β π) β βπ β π΅ π β π ) |
216 | 215 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ β π βπ β π΅ π β π ) |
217 | 92 | rexbidv 3176 |
. . . . . . . . . . . . . 14
β’ (π = π΄ β (βπ β π΅ (π΄ +no π) β (π +no π ) β βπ β π΅ (π΄ +no π) β (π΄ +no π ))) |
218 | 217 | rexsng 4636 |
. . . . . . . . . . . . 13
β’ (π΄ β On β (βπ β {π΄}βπ β π΅ (π΄ +no π) β (π +no π ) β βπ β π΅ (π΄ +no π) β (π΄ +no π ))) |
219 | 1, 218 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (βπ β {π΄}βπ β π΅ (π΄ +no π) β (π +no π ) β βπ β π΅ (π΄ +no π) β (π΄ +no π ))) |
220 | 219 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (βπ β {π΄}βπ β π΅ (π΄ +no π) β (π +no π ) β βπ β π΅ (π΄ +no π) β (π΄ +no π ))) |
221 | | sseq2 3971 |
. . . . . . . . . . . . . 14
β’ (π = (π +no π ) β ((π΄ +no π) β π β (π΄ +no π) β (π +no π ))) |
222 | 221 | imaeqexov 7593 |
. . . . . . . . . . . . 13
β’ (( +no Fn
(On Γ On) β§ ({π΄}
Γ π΅) β (On
Γ On)) β (βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β βπ β {π΄}βπ β π΅ (π΄ +no π) β (π +no π ))) |
223 | 5, 106, 222 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β (βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β βπ β {π΄}βπ β π΅ (π΄ +no π) β (π +no π ))) |
224 | 223 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β βπ β {π΄}βπ β π΅ (π΄ +no π) β (π +no π ))) |
225 | 76 | sselda 3945 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π β On) |
226 | 225 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β π΅) β π β On) |
227 | 67 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π΅ β On) |
228 | 227 | sselda 3945 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β π΅) β π β On) |
229 | 1 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β π΅) β π΄ β On) |
230 | 226, 228,
229, 80 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β π΅) β (π β π β (π΄ +no π) β (π΄ +no π ))) |
231 | 230 | rexbidva 3174 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (βπ β π΅ π β π β βπ β π΅ (π΄ +no π) β (π΄ +no π ))) |
232 | 220, 224,
231 | 3bitr4d 311 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β βπ β π΅ π β π )) |
233 | 232 | ralbidva 3173 |
. . . . . . . . 9
β’ (π β (βπ β π βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β βπ β π βπ β π΅ π β π )) |
234 | 216, 233 | mpbird 257 |
. . . . . . . 8
β’ (π β βπ β π βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π) |
235 | | orc 866 |
. . . . . . . . 9
β’
(βπ β (
+no β ({π΄} Γ
π΅))(π΄ +no π) β π β (βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π΄ +no π) β π)) |
236 | 235 | ralimi 3087 |
. . . . . . . 8
β’
(βπ β
π βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β βπ β π (βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π΄ +no π) β π)) |
237 | 234, 236 | syl 17 |
. . . . . . 7
β’ (π β βπ β π (βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π΄ +no π) β π)) |
238 | | rexun 4151 |
. . . . . . . 8
β’
(βπ β ((
+no β ({π΄} Γ
π΅)) βͺ ( +no β
(π΄ Γ {π΅})))(π΄ +no π) β π β (βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π΄ +no π) β π)) |
239 | 238 | ralbii 3097 |
. . . . . . 7
β’
(βπ β
π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π΄ +no π) β π β βπ β π (βπ β ( +no β ({π΄} Γ π΅))(π΄ +no π) β π β¨ βπ β ( +no β (π΄ Γ {π΅}))(π΄ +no π) β π)) |
240 | 237, 239 | sylibr 233 |
. . . . . 6
β’ (π β βπ β π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π΄ +no π) β π) |
241 | 111 | sseq1d 3976 |
. . . . . . . . . 10
β’ (π = π΄ β ((π +no π) β π β (π΄ +no π) β π)) |
242 | 241 | rexbidv 3176 |
. . . . . . . . 9
β’ (π = π΄ β (βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π β βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π΄ +no π) β π)) |
243 | 242 | ralbidv 3175 |
. . . . . . . 8
β’ (π = π΄ β (βπ β π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π β βπ β π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π΄ +no π) β π)) |
244 | 243 | ralsng 4635 |
. . . . . . 7
β’ (π΄ β On β (βπ β {π΄}βπ β π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π β βπ β π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π΄ +no π) β π)) |
245 | 1, 244 | syl 17 |
. . . . . 6
β’ (π β (βπ β {π΄}βπ β π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π β βπ β π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π΄ +no π) β π)) |
246 | 240, 245 | mpbird 257 |
. . . . 5
β’ (π β βπ β {π΄}βπ β π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π) |
247 | 205 | imaeqalov 7594 |
. . . . . 6
β’ (( +no Fn
(On Γ On) β§ ({π΄}
Γ π) β (On
Γ On)) β (βπ β ( +no β ({π΄} Γ π))βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π β βπ β {π΄}βπ β π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π)) |
248 | 5, 87, 247 | sylancr 588 |
. . . . 5
β’ (π β (βπ β ( +no β ({π΄} Γ π))βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π β βπ β {π΄}βπ β π βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))(π +no π) β π)) |
249 | 246, 248 | mpbird 257 |
. . . 4
β’ (π β βπ β ( +no β ({π΄} Γ π))βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π) |
250 | | ralunb 4152 |
. . . 4
β’
(βπ β ((
+no β (π Γ
{π΅})) βͺ ( +no β
({π΄} Γ π)))βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π β (βπ β ( +no β (π Γ {π΅}))βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π β§ βπ β ( +no β ({π΄} Γ π))βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π)) |
251 | 208, 249,
250 | sylanbrc 584 |
. . 3
β’ (π β βπ β (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π)))βπ β (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅})))π β π) |
252 | 30, 64, 168, 251 | cofon2 8620 |
. 2
β’ (π β β© {π€
β On β£ (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅}))) β π€} = β© {π§ β On β£ (( +no
β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π))) β π§}) |
253 | 4, 252 | eqtrd 2777 |
1
β’ (π β (π΄ +no π΅) = β© {π§ β On β£ (( +no
β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π))) β π§}) |