Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β π΄ β On) |
2 | | naddcl 8624 |
. . . 4
β’ ((π΅ β On β§ πΆ β On) β (π΅ +no πΆ) β On) |
3 | 2 | 3adant1 1131 |
. . 3
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΅ +no πΆ) β On) |
4 | | intmin 4930 |
. . . . 5
β’ (π΄ β On β β© {π
β On β£ π΄ β
π} = π΄) |
5 | 4 | eqcomd 2743 |
. . . 4
β’ (π΄ β On β π΄ = β©
{π β On β£ π΄ β π}) |
6 | 5 | 3ad2ant1 1134 |
. . 3
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β π΄ = β©
{π β On β£ π΄ β π}) |
7 | | naddov3 8627 |
. . . 4
β’ ((π΅ β On β§ πΆ β On) β (π΅ +no πΆ) = β© {π β On β£ (( +no
β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ}))) β π}) |
8 | 7 | 3adant1 1131 |
. . 3
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΅ +no πΆ) = β© {π β On β£ (( +no
β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ}))) β π}) |
9 | 1, 3, 6, 8 | naddunif 8638 |
. 2
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ +no (π΅ +no πΆ)) = β© {π₯ β On β£ (( +no
β (π΄ Γ {(π΅ +no πΆ)})) βͺ ( +no β ({π΄} Γ (( +no β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ})))))) β π₯}) |
10 | | 3anass 1096 |
. . . . . 6
β’ ((( +no
β (π΄ Γ {(π΅ +no πΆ)})) β π₯ β§ ( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ})))) β π₯ β§ ( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) β π₯) β (( +no β (π΄ Γ {(π΅ +no πΆ)})) β π₯ β§ (( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ})))) β π₯ β§ ( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) β π₯))) |
11 | | unss 4145 |
. . . . . . . 8
β’ ((( +no
β ({π΄} Γ ( +no
β ({π΅} Γ πΆ)))) β π₯ β§ ( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ})))) β π₯) β (( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) βͺ ( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ}))))) β π₯) |
12 | | ancom 462 |
. . . . . . . 8
β’ ((( +no
β ({π΄} Γ ( +no
β (π΅ Γ {πΆ})))) β π₯ β§ ( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) β π₯) β (( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) β π₯ β§ ( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ})))) β π₯)) |
13 | | xpundi 5701 |
. . . . . . . . . . 11
β’ ({π΄} Γ (( +no β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ})))) = (({π΄} Γ ( +no β ({π΅} Γ πΆ))) βͺ ({π΄} Γ ( +no β (π΅ Γ {πΆ})))) |
14 | 13 | imaeq2i 6012 |
. . . . . . . . . 10
β’ ( +no
β ({π΄} Γ (( +no
β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ}))))) = ( +no β (({π΄} Γ ( +no β ({π΅} Γ πΆ))) βͺ ({π΄} Γ ( +no β (π΅ Γ {πΆ}))))) |
15 | | imaundi 6103 |
. . . . . . . . . 10
β’ ( +no
β (({π΄} Γ ( +no
β ({π΅} Γ πΆ))) βͺ ({π΄} Γ ( +no β (π΅ Γ {πΆ}))))) = (( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) βͺ ( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ}))))) |
16 | 14, 15 | eqtri 2765 |
. . . . . . . . 9
β’ ( +no
β ({π΄} Γ (( +no
β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ}))))) = (( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) βͺ ( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ}))))) |
17 | 16 | sseq1i 3973 |
. . . . . . . 8
β’ (( +no
β ({π΄} Γ (( +no
β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ}))))) β π₯ β (( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) βͺ ( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ}))))) β π₯) |
18 | 11, 12, 17 | 3bitr4i 303 |
. . . . . . 7
β’ ((( +no
β ({π΄} Γ ( +no
β (π΅ Γ {πΆ})))) β π₯ β§ ( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) β π₯) β ( +no β ({π΄} Γ (( +no β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ}))))) β π₯) |
19 | 18 | anbi2i 624 |
. . . . . 6
β’ ((( +no
β (π΄ Γ {(π΅ +no πΆ)})) β π₯ β§ (( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ})))) β π₯ β§ ( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) β π₯)) β (( +no β (π΄ Γ {(π΅ +no πΆ)})) β π₯ β§ ( +no β ({π΄} Γ (( +no β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ}))))) β π₯)) |
20 | | unss 4145 |
. . . . . 6
β’ ((( +no
β (π΄ Γ {(π΅ +no πΆ)})) β π₯ β§ ( +no β ({π΄} Γ (( +no β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ}))))) β π₯) β (( +no β (π΄ Γ {(π΅ +no πΆ)})) βͺ ( +no β ({π΄} Γ (( +no β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ})))))) β π₯) |
21 | 10, 19, 20 | 3bitrri 298 |
. . . . 5
β’ ((( +no
β (π΄ Γ {(π΅ +no πΆ)})) βͺ ( +no β ({π΄} Γ (( +no β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ})))))) β π₯ β (( +no β (π΄ Γ {(π΅ +no πΆ)})) β π₯ β§ ( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ})))) β π₯ β§ ( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) β π₯)) |
22 | | naddfn 8622 |
. . . . . . . . 9
β’ +no Fn
(On Γ On) |
23 | | fnfun 6603 |
. . . . . . . . 9
β’ ( +no Fn
(On Γ On) β Fun +no ) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . 8
β’ Fun
+no |
25 | | onss 7720 |
. . . . . . . . . . 11
β’ (π΄ β On β π΄ β On) |
26 | 25 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β π΄ β On) |
27 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β (π΅ +no πΆ) β On) |
28 | 27 | snssd 4770 |
. . . . . . . . . 10
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β {(π΅ +no πΆ)} β On) |
29 | | xpss12 5649 |
. . . . . . . . . 10
β’ ((π΄ β On β§ {(π΅ +no πΆ)} β On) β (π΄ Γ {(π΅ +no πΆ)}) β (On Γ
On)) |
30 | 26, 28, 29 | syl2an2r 684 |
. . . . . . . . 9
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β (π΄ Γ {(π΅ +no πΆ)}) β (On Γ
On)) |
31 | 22 | fndmi 6607 |
. . . . . . . . 9
β’ dom +no =
(On Γ On) |
32 | 30, 31 | sseqtrrdi 3996 |
. . . . . . . 8
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β (π΄ Γ {(π΅ +no πΆ)}) β dom +no ) |
33 | | funimassov 7532 |
. . . . . . . 8
β’ ((Fun +no
β§ (π΄ Γ {(π΅ +no πΆ)}) β dom +no ) β (( +no β
(π΄ Γ {(π΅ +no πΆ)})) β π₯ β βπ β π΄ βπ β {(π΅ +no πΆ)} (π +no π) β π₯)) |
34 | 24, 32, 33 | sylancr 588 |
. . . . . . 7
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β (( +no
β (π΄ Γ {(π΅ +no πΆ)})) β π₯ β βπ β π΄ βπ β {(π΅ +no πΆ)} (π +no π) β π₯)) |
35 | | ovex 7391 |
. . . . . . . . 9
β’ (π΅ +no πΆ) β V |
36 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π = (π΅ +no πΆ) β (π +no π) = (π +no (π΅ +no πΆ))) |
37 | 36 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = (π΅ +no πΆ) β ((π +no π) β π₯ β (π +no (π΅ +no πΆ)) β π₯)) |
38 | 35, 37 | ralsn 4643 |
. . . . . . . 8
β’
(βπ β
{(π΅ +no πΆ)} (π +no π) β π₯ β (π +no (π΅ +no πΆ)) β π₯) |
39 | 38 | ralbii 3097 |
. . . . . . 7
β’
(βπ β
π΄ βπ β {(π΅ +no πΆ)} (π +no π) β π₯ β βπ β π΄ (π +no (π΅ +no πΆ)) β π₯) |
40 | 34, 39 | bitrdi 287 |
. . . . . 6
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β (( +no
β (π΄ Γ {(π΅ +no πΆ)})) β π₯ β βπ β π΄ (π +no (π΅ +no πΆ)) β π₯)) |
41 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β π΄ β On) |
42 | 41 | snssd 4770 |
. . . . . . . . . 10
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β {π΄} β On) |
43 | | imassrn 6025 |
. . . . . . . . . . 11
β’ ( +no
β (π΅ Γ {πΆ})) β ran
+no |
44 | | naddf 8628 |
. . . . . . . . . . . 12
β’ +no :(On
Γ On)βΆOn |
45 | | frn 6676 |
. . . . . . . . . . . 12
β’ ( +no
:(On Γ On)βΆOn β ran +no β On) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . . . 11
β’ ran +no
β On |
47 | 43, 46 | sstri 3954 |
. . . . . . . . . 10
β’ ( +no
β (π΅ Γ {πΆ})) β On |
48 | | xpss12 5649 |
. . . . . . . . . 10
β’ (({π΄} β On β§ ( +no β
(π΅ Γ {πΆ})) β On) β ({π΄} Γ ( +no β (π΅ Γ {πΆ}))) β (On Γ
On)) |
49 | 42, 47, 48 | sylancl 587 |
. . . . . . . . 9
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β ({π΄} Γ ( +no β (π΅ Γ {πΆ}))) β (On Γ
On)) |
50 | 49, 31 | sseqtrrdi 3996 |
. . . . . . . 8
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β ({π΄} Γ ( +no β (π΅ Γ {πΆ}))) β dom +no ) |
51 | | funimassov 7532 |
. . . . . . . 8
β’ ((Fun +no
β§ ({π΄} Γ ( +no
β (π΅ Γ {πΆ}))) β dom +no ) β ((
+no β ({π΄} Γ (
+no β (π΅ Γ
{πΆ})))) β π₯ β βπ β {π΄}βπ β ( +no β (π΅ Γ {πΆ}))(π +no π) β π₯)) |
52 | 24, 50, 51 | sylancr 588 |
. . . . . . 7
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β (( +no
β ({π΄} Γ ( +no
β (π΅ Γ {πΆ})))) β π₯ β βπ β {π΄}βπ β ( +no β (π΅ Γ {πΆ}))(π +no π) β π₯)) |
53 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π = π΄ β (π +no π) = (π΄ +no π)) |
54 | 53 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π = π΄ β ((π +no π) β π₯ β (π΄ +no π) β π₯)) |
55 | 54 | ralbidv 3175 |
. . . . . . . . 9
β’ (π = π΄ β (βπ β ( +no β (π΅ Γ {πΆ}))(π +no π) β π₯ β βπ β ( +no β (π΅ Γ {πΆ}))(π΄ +no π) β π₯)) |
56 | 55 | ralsng 4635 |
. . . . . . . 8
β’ (π΄ β On β (βπ β {π΄}βπ β ( +no β (π΅ Γ {πΆ}))(π +no π) β π₯ β βπ β ( +no β (π΅ Γ {πΆ}))(π΄ +no π) β π₯)) |
57 | 41, 56 | syl 17 |
. . . . . . 7
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β
(βπ β {π΄}βπ β ( +no β (π΅ Γ {πΆ}))(π +no π) β π₯ β βπ β ( +no β (π΅ Γ {πΆ}))(π΄ +no π) β π₯)) |
58 | | onss 7720 |
. . . . . . . . . . 11
β’ (π΅ β On β π΅ β On) |
59 | 58 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β π΅ β On) |
60 | | simpl3 1194 |
. . . . . . . . . . 11
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β πΆ β On) |
61 | 60 | snssd 4770 |
. . . . . . . . . 10
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β {πΆ} β On) |
62 | | xpss12 5649 |
. . . . . . . . . 10
β’ ((π΅ β On β§ {πΆ} β On) β (π΅ Γ {πΆ}) β (On Γ On)) |
63 | 59, 61, 62 | syl2an2r 684 |
. . . . . . . . 9
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β (π΅ Γ {πΆ}) β (On Γ On)) |
64 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π = (π +no π) β (π΄ +no π) = (π΄ +no (π +no π))) |
65 | 64 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π = (π +no π) β ((π΄ +no π) β π₯ β (π΄ +no (π +no π)) β π₯)) |
66 | 65 | imaeqalov 7594 |
. . . . . . . . 9
β’ (( +no Fn
(On Γ On) β§ (π΅
Γ {πΆ}) β (On
Γ On)) β (βπ β ( +no β (π΅ Γ {πΆ}))(π΄ +no π) β π₯ β βπ β π΅ βπ β {πΆ} (π΄ +no (π +no π)) β π₯)) |
67 | 22, 63, 66 | sylancr 588 |
. . . . . . . 8
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β
(βπ β ( +no
β (π΅ Γ {πΆ}))(π΄ +no π) β π₯ β βπ β π΅ βπ β {πΆ} (π΄ +no (π +no π)) β π₯)) |
68 | | oveq2 7366 |
. . . . . . . . . . . . 13
β’ (π = πΆ β (π +no π) = (π +no πΆ)) |
69 | 68 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π = πΆ β (π΄ +no (π +no π)) = (π΄ +no (π +no πΆ))) |
70 | 69 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π = πΆ β ((π΄ +no (π +no π)) β π₯ β (π΄ +no (π +no πΆ)) β π₯)) |
71 | 70 | ralsng 4635 |
. . . . . . . . . 10
β’ (πΆ β On β (βπ β {πΆ} (π΄ +no (π +no π)) β π₯ β (π΄ +no (π +no πΆ)) β π₯)) |
72 | 60, 71 | syl 17 |
. . . . . . . . 9
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β
(βπ β {πΆ} (π΄ +no (π +no π)) β π₯ β (π΄ +no (π +no πΆ)) β π₯)) |
73 | 72 | ralbidv 3175 |
. . . . . . . 8
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β
(βπ β π΅ βπ β {πΆ} (π΄ +no (π +no π)) β π₯ β βπ β π΅ (π΄ +no (π +no πΆ)) β π₯)) |
74 | 67, 73 | bitrd 279 |
. . . . . . 7
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β
(βπ β ( +no
β (π΅ Γ {πΆ}))(π΄ +no π) β π₯ β βπ β π΅ (π΄ +no (π +no πΆ)) β π₯)) |
75 | 52, 57, 74 | 3bitrd 305 |
. . . . . 6
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β (( +no
β ({π΄} Γ ( +no
β (π΅ Γ {πΆ})))) β π₯ β βπ β π΅ (π΄ +no (π +no πΆ)) β π₯)) |
76 | | imassrn 6025 |
. . . . . . . . . . 11
β’ ( +no
β ({π΅} Γ πΆ)) β ran
+no |
77 | 76, 46 | sstri 3954 |
. . . . . . . . . 10
β’ ( +no
β ({π΅} Γ πΆ)) β On |
78 | | xpss12 5649 |
. . . . . . . . . 10
β’ (({π΄} β On β§ ( +no β
({π΅} Γ πΆ)) β On) β ({π΄} Γ ( +no β ({π΅} Γ πΆ))) β (On Γ
On)) |
79 | 42, 77, 78 | sylancl 587 |
. . . . . . . . 9
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β ({π΄} Γ ( +no β ({π΅} Γ πΆ))) β (On Γ
On)) |
80 | 79, 31 | sseqtrrdi 3996 |
. . . . . . . 8
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β ({π΄} Γ ( +no β ({π΅} Γ πΆ))) β dom +no ) |
81 | | funimassov 7532 |
. . . . . . . 8
β’ ((Fun +no
β§ ({π΄} Γ ( +no
β ({π΅} Γ πΆ))) β dom +no ) β ((
+no β ({π΄} Γ (
+no β ({π΅} Γ
πΆ)))) β π₯ β βπ β {π΄}βπ β ( +no β ({π΅} Γ πΆ))(π +no π) β π₯)) |
82 | 24, 80, 81 | sylancr 588 |
. . . . . . 7
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β (( +no
β ({π΄} Γ ( +no
β ({π΅} Γ πΆ)))) β π₯ β βπ β {π΄}βπ β ( +no β ({π΅} Γ πΆ))(π +no π) β π₯)) |
83 | 54 | ralbidv 3175 |
. . . . . . . . 9
β’ (π = π΄ β (βπ β ( +no β ({π΅} Γ πΆ))(π +no π) β π₯ β βπ β ( +no β ({π΅} Γ πΆ))(π΄ +no π) β π₯)) |
84 | 83 | ralsng 4635 |
. . . . . . . 8
β’ (π΄ β On β (βπ β {π΄}βπ β ( +no β ({π΅} Γ πΆ))(π +no π) β π₯ β βπ β ( +no β ({π΅} Γ πΆ))(π΄ +no π) β π₯)) |
85 | 41, 84 | syl 17 |
. . . . . . 7
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β
(βπ β {π΄}βπ β ( +no β ({π΅} Γ πΆ))(π +no π) β π₯ β βπ β ( +no β ({π΅} Γ πΆ))(π΄ +no π) β π₯)) |
86 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β π΅ β On) |
87 | 86 | snssd 4770 |
. . . . . . . . . 10
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β {π΅} β On) |
88 | | onss 7720 |
. . . . . . . . . . . 12
β’ (πΆ β On β πΆ β On) |
89 | 88 | 3ad2ant3 1136 |
. . . . . . . . . . 11
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β πΆ β On) |
90 | 89 | adantr 482 |
. . . . . . . . . 10
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β πΆ β On) |
91 | | xpss12 5649 |
. . . . . . . . . 10
β’ (({π΅} β On β§ πΆ β On) β ({π΅} Γ πΆ) β (On Γ On)) |
92 | 87, 90, 91 | syl2anc 585 |
. . . . . . . . 9
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β ({π΅} Γ πΆ) β (On Γ On)) |
93 | 65 | imaeqalov 7594 |
. . . . . . . . 9
β’ (( +no Fn
(On Γ On) β§ ({π΅}
Γ πΆ) β (On
Γ On)) β (βπ β ( +no β ({π΅} Γ πΆ))(π΄ +no π) β π₯ β βπ β {π΅}βπ β πΆ (π΄ +no (π +no π)) β π₯)) |
94 | 22, 92, 93 | sylancr 588 |
. . . . . . . 8
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β
(βπ β ( +no
β ({π΅} Γ πΆ))(π΄ +no π) β π₯ β βπ β {π΅}βπ β πΆ (π΄ +no (π +no π)) β π₯)) |
95 | | oveq1 7365 |
. . . . . . . . . . . . 13
β’ (π = π΅ β (π +no π) = (π΅ +no π)) |
96 | 95 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π = π΅ β (π΄ +no (π +no π)) = (π΄ +no (π΅ +no π))) |
97 | 96 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π = π΅ β ((π΄ +no (π +no π)) β π₯ β (π΄ +no (π΅ +no π)) β π₯)) |
98 | 97 | ralbidv 3175 |
. . . . . . . . . 10
β’ (π = π΅ β (βπ β πΆ (π΄ +no (π +no π)) β π₯ β βπ β πΆ (π΄ +no (π΅ +no π)) β π₯)) |
99 | 98 | ralsng 4635 |
. . . . . . . . 9
β’ (π΅ β On β (βπ β {π΅}βπ β πΆ (π΄ +no (π +no π)) β π₯ β βπ β πΆ (π΄ +no (π΅ +no π)) β π₯)) |
100 | 86, 99 | syl 17 |
. . . . . . . 8
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β
(βπ β {π΅}βπ β πΆ (π΄ +no (π +no π)) β π₯ β βπ β πΆ (π΄ +no (π΅ +no π)) β π₯)) |
101 | 94, 100 | bitrd 279 |
. . . . . . 7
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β
(βπ β ( +no
β ({π΅} Γ πΆ))(π΄ +no π) β π₯ β βπ β πΆ (π΄ +no (π΅ +no π)) β π₯)) |
102 | 82, 85, 101 | 3bitrd 305 |
. . . . . 6
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β (( +no
β ({π΄} Γ ( +no
β ({π΅} Γ πΆ)))) β π₯ β βπ β πΆ (π΄ +no (π΅ +no π)) β π₯)) |
103 | 40, 75, 102 | 3anbi123d 1437 |
. . . . 5
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β ((( +no
β (π΄ Γ {(π΅ +no πΆ)})) β π₯ β§ ( +no β ({π΄} Γ ( +no β (π΅ Γ {πΆ})))) β π₯ β§ ( +no β ({π΄} Γ ( +no β ({π΅} Γ πΆ)))) β π₯) β (βπ β π΄ (π +no (π΅ +no πΆ)) β π₯ β§ βπ β π΅ (π΄ +no (π +no πΆ)) β π₯ β§ βπ β πΆ (π΄ +no (π΅ +no π)) β π₯))) |
104 | 21, 103 | bitrid 283 |
. . . 4
β’ (((π΄ β On β§ π΅ β On β§ πΆ β On) β§ π₯ β On) β ((( +no
β (π΄ Γ {(π΅ +no πΆ)})) βͺ ( +no β ({π΄} Γ (( +no β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ})))))) β π₯ β (βπ β π΄ (π +no (π΅ +no πΆ)) β π₯ β§ βπ β π΅ (π΄ +no (π +no πΆ)) β π₯ β§ βπ β πΆ (π΄ +no (π΅ +no π)) β π₯))) |
105 | 104 | rabbidva 3415 |
. . 3
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β {π₯ β On β£ (( +no
β (π΄ Γ {(π΅ +no πΆ)})) βͺ ( +no β ({π΄} Γ (( +no β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ})))))) β π₯} = {π₯ β On β£ (βπ β π΄ (π +no (π΅ +no πΆ)) β π₯ β§ βπ β π΅ (π΄ +no (π +no πΆ)) β π₯ β§ βπ β πΆ (π΄ +no (π΅ +no π)) β π₯)}) |
106 | 105 | inteqd 4913 |
. 2
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β β© {π₯
β On β£ (( +no β (π΄ Γ {(π΅ +no πΆ)})) βͺ ( +no β ({π΄} Γ (( +no β ({π΅} Γ πΆ)) βͺ ( +no β (π΅ Γ {πΆ})))))) β π₯} = β© {π₯ β On β£
(βπ β π΄ (π +no (π΅ +no πΆ)) β π₯ β§ βπ β π΅ (π΄ +no (π +no πΆ)) β π₯ β§ βπ β πΆ (π΄ +no (π΅ +no π)) β π₯)}) |
107 | 9, 106 | eqtrd 2777 |
1
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ +no (π΅ +no πΆ)) = β© {π₯ β On β£
(βπ β π΄ (π +no (π΅ +no πΆ)) β π₯ β§ βπ β π΅ (π΄ +no (π +no πΆ)) β π₯ β§ βπ β πΆ (π΄ +no (π΅ +no π)) β π₯)}) |