Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . 6
β’ ((π β§ π
β V) β π
β V) |
2 | | nn0ex 12478 |
. . . . . . 7
β’
β0 β V |
3 | | ovex 7442 |
. . . . . . 7
β’ (π
βππ) β V |
4 | 2, 3 | iunex 7955 |
. . . . . 6
β’ βͺ π β β0 (π
βππ) β V |
5 | | oveq1 7416 |
. . . . . . . 8
β’ (π = π
β (πβππ) = (π
βππ)) |
6 | 5 | iuneq2d 5027 |
. . . . . . 7
β’ (π = π
β βͺ
π β
β0 (πβππ) = βͺ π β β0
(π
βππ)) |
7 | | eqid 2733 |
. . . . . . 7
β’ (π β V β¦ βͺ π β β0 (πβππ)) = (π β V β¦ βͺ π β β0 (πβππ)) |
8 | 6, 7 | fvmptg 6997 |
. . . . . 6
β’ ((π
β V β§ βͺ π β β0 (π
βππ) β V) β ((π β V β¦ βͺ π β β0 (πβππ))βπ
) = βͺ
π β
β0 (π
βππ)) |
9 | 1, 4, 8 | sylancl 587 |
. . . . 5
β’ ((π β§ π
β V) β ((π β V β¦ βͺ π β β0 (πβππ))βπ
) = βͺ
π β
β0 (π
βππ)) |
10 | 9 | ex 414 |
. . . 4
β’ (π β (π
β V β ((π β V β¦ βͺ π β β0 (πβππ))βπ
) = βͺ
π β
β0 (π
βππ))) |
11 | | iun0 5066 |
. . . . . 6
β’ βͺ π β β0 β
=
β
|
12 | 11 | a1i 11 |
. . . . 5
β’ (Β¬
π
β V β βͺ π β β0 β
=
β
) |
13 | | reldmrelexp 14968 |
. . . . . . 7
β’ Rel dom
βπ |
14 | 13 | ovprc1 7448 |
. . . . . 6
β’ (Β¬
π
β V β (π
βππ) = β
) |
15 | 14 | iuneq2d 5027 |
. . . . 5
β’ (Β¬
π
β V β βͺ π β β0 (π
βππ) = βͺ π β β0
β
) |
16 | | fvprc 6884 |
. . . . 5
β’ (Β¬
π
β V β ((π β V β¦ βͺ π β β0 (πβππ))βπ
) = β
) |
17 | 12, 15, 16 | 3eqtr4rd 2784 |
. . . 4
β’ (Β¬
π
β V β ((π β V β¦ βͺ π β β0 (πβππ))βπ
) = βͺ
π β
β0 (π
βππ)) |
18 | 10, 17 | pm2.61d1 180 |
. . 3
β’ (π β ((π β V β¦ βͺ π β β0 (πβππ))βπ
) = βͺ
π β
β0 (π
βππ)) |
19 | | breq 5151 |
. . . 4
β’ (((π β V β¦ βͺ π β β0 (πβππ))βπ
) = βͺ
π β
β0 (π
βππ) β (π΄((π β V β¦ βͺ π β β0 (πβππ))βπ
)π΅ β π΄βͺ π β β0
(π
βππ)π΅)) |
20 | | eliun 5002 |
. . . . . 6
β’
(β¨π΄, π΅β© β βͺ π β β0 (π
βππ) β βπ β β0
β¨π΄, π΅β© β (π
βππ)) |
21 | 20 | a1i 11 |
. . . . 5
β’ (π β (β¨π΄, π΅β© β βͺ π β β0 (π
βππ) β βπ β β0
β¨π΄, π΅β© β (π
βππ))) |
22 | | df-br 5150 |
. . . . 5
β’ (π΄βͺ π β β0 (π
βππ)π΅ β β¨π΄, π΅β© β βͺ π β β0 (π
βππ)) |
23 | | df-br 5150 |
. . . . . 6
β’ (π΄(π
βππ)π΅ β β¨π΄, π΅β© β (π
βππ)) |
24 | 23 | rexbii 3095 |
. . . . 5
β’
(βπ β
β0 π΄(π
βππ)π΅ β βπ β β0 β¨π΄, π΅β© β (π
βππ)) |
25 | 21, 22, 24 | 3bitr4g 314 |
. . . 4
β’ (π β (π΄βͺ π β β0
(π
βππ)π΅ β βπ β β0 π΄(π
βππ)π΅)) |
26 | 19, 25 | sylan9bb 511 |
. . 3
β’ ((((π β V β¦ βͺ π β β0 (πβππ))βπ
) = βͺ
π β
β0 (π
βππ) β§ π) β (π΄((π β V β¦ βͺ π β β0 (πβππ))βπ
)π΅ β βπ β β0 π΄(π
βππ)π΅)) |
27 | 18, 26 | mpancom 687 |
. 2
β’ (π β (π΄((π β V β¦ βͺ π β β0 (πβππ))βπ
)π΅ β βπ β β0 π΄(π
βππ)π΅)) |
28 | | df-rtrclrec 15003 |
. . 3
β’ t*rec =
(π β V β¦
βͺ π β β0 (πβππ)) |
29 | | fveq1 6891 |
. . . . . 6
β’ (t*rec =
(π β V β¦
βͺ π β β0 (πβππ)) β (t*recβπ
) = ((π β V β¦ βͺ π β β0 (πβππ))βπ
)) |
30 | 29 | breqd 5160 |
. . . . 5
β’ (t*rec =
(π β V β¦
βͺ π β β0 (πβππ)) β (π΄(t*recβπ
)π΅ β π΄((π β V β¦ βͺ π β β0 (πβππ))βπ
)π΅)) |
31 | 30 | bibi1d 344 |
. . . 4
β’ (t*rec =
(π β V β¦
βͺ π β β0 (πβππ)) β ((π΄(t*recβπ
)π΅ β βπ β β0 π΄(π
βππ)π΅) β (π΄((π β V β¦ βͺ π β β0 (πβππ))βπ
)π΅ β βπ β β0 π΄(π
βππ)π΅))) |
32 | 31 | imbi2d 341 |
. . 3
β’ (t*rec =
(π β V β¦
βͺ π β β0 (πβππ)) β ((π β (π΄(t*recβπ
)π΅ β βπ β β0 π΄(π
βππ)π΅)) β (π β (π΄((π β V β¦ βͺ π β β0 (πβππ))βπ
)π΅ β βπ β β0 π΄(π
βππ)π΅)))) |
33 | 28, 32 | ax-mp 5 |
. 2
β’ ((π β (π΄(t*recβπ
)π΅ β βπ β β0 π΄(π
βππ)π΅)) β (π β (π΄((π β V β¦ βͺ π β β0 (πβππ))βπ
)π΅ β βπ β β0 π΄(π
βππ)π΅))) |
34 | 27, 33 | mpbir 230 |
1
β’ (π β (π΄(t*recβπ
)π΅ β βπ β β0 π΄(π
βππ)π΅)) |