Step | Hyp | Ref
| Expression |
1 | | elsuci 6431 |
. 2
β’ (π΅ β suc dom recs(πΉ) β (π΅ β dom recs(πΉ) β¨ π΅ = dom recs(πΉ))) |
2 | | tfrlem.1 |
. . . . . . . . 9
β’ π΄ = {π β£ βπ₯ β On (π Fn π₯ β§ βπ¦ β π₯ (πβπ¦) = (πΉβ(π βΎ π¦)))} |
3 | | tfrlem.3 |
. . . . . . . . 9
β’ πΆ = (recs(πΉ) βͺ {β¨dom recs(πΉ), (πΉβrecs(πΉ))β©}) |
4 | 2, 3 | tfrlem10 8390 |
. . . . . . . 8
β’ (dom
recs(πΉ) β On β
πΆ Fn suc dom recs(πΉ)) |
5 | | fnfun 6649 |
. . . . . . . 8
β’ (πΆ Fn suc dom recs(πΉ) β Fun πΆ) |
6 | 4, 5 | syl 17 |
. . . . . . 7
β’ (dom
recs(πΉ) β On β
Fun πΆ) |
7 | | ssun1 4172 |
. . . . . . . . 9
β’
recs(πΉ) β
(recs(πΉ) βͺ {β¨dom
recs(πΉ), (πΉβrecs(πΉ))β©}) |
8 | 7, 3 | sseqtrri 4019 |
. . . . . . . 8
β’
recs(πΉ) β
πΆ |
9 | 2 | tfrlem9 8388 |
. . . . . . . . 9
β’ (π΅ β dom recs(πΉ) β (recs(πΉ)βπ΅) = (πΉβ(recs(πΉ) βΎ π΅))) |
10 | | funssfv 6912 |
. . . . . . . . . . . 12
β’ ((Fun
πΆ β§ recs(πΉ) β πΆ β§ π΅ β dom recs(πΉ)) β (πΆβπ΅) = (recs(πΉ)βπ΅)) |
11 | 10 | 3expa 1117 |
. . . . . . . . . . 11
β’ (((Fun
πΆ β§ recs(πΉ) β πΆ) β§ π΅ β dom recs(πΉ)) β (πΆβπ΅) = (recs(πΉ)βπ΅)) |
12 | 11 | adantrl 713 |
. . . . . . . . . 10
β’ (((Fun
πΆ β§ recs(πΉ) β πΆ) β§ (dom recs(πΉ) β On β§ π΅ β dom recs(πΉ))) β (πΆβπ΅) = (recs(πΉ)βπ΅)) |
13 | | onelss 6406 |
. . . . . . . . . . . 12
β’ (dom
recs(πΉ) β On β
(π΅ β dom recs(πΉ) β π΅ β dom recs(πΉ))) |
14 | 13 | imp 406 |
. . . . . . . . . . 11
β’ ((dom
recs(πΉ) β On β§
π΅ β dom recs(πΉ)) β π΅ β dom recs(πΉ)) |
15 | | fun2ssres 6593 |
. . . . . . . . . . . . 13
β’ ((Fun
πΆ β§ recs(πΉ) β πΆ β§ π΅ β dom recs(πΉ)) β (πΆ βΎ π΅) = (recs(πΉ) βΎ π΅)) |
16 | 15 | 3expa 1117 |
. . . . . . . . . . . 12
β’ (((Fun
πΆ β§ recs(πΉ) β πΆ) β§ π΅ β dom recs(πΉ)) β (πΆ βΎ π΅) = (recs(πΉ) βΎ π΅)) |
17 | 16 | fveq2d 6895 |
. . . . . . . . . . 11
β’ (((Fun
πΆ β§ recs(πΉ) β πΆ) β§ π΅ β dom recs(πΉ)) β (πΉβ(πΆ βΎ π΅)) = (πΉβ(recs(πΉ) βΎ π΅))) |
18 | 14, 17 | sylan2 592 |
. . . . . . . . . 10
β’ (((Fun
πΆ β§ recs(πΉ) β πΆ) β§ (dom recs(πΉ) β On β§ π΅ β dom recs(πΉ))) β (πΉβ(πΆ βΎ π΅)) = (πΉβ(recs(πΉ) βΎ π΅))) |
19 | 12, 18 | eqeq12d 2747 |
. . . . . . . . 9
β’ (((Fun
πΆ β§ recs(πΉ) β πΆ) β§ (dom recs(πΉ) β On β§ π΅ β dom recs(πΉ))) β ((πΆβπ΅) = (πΉβ(πΆ βΎ π΅)) β (recs(πΉ)βπ΅) = (πΉβ(recs(πΉ) βΎ π΅)))) |
20 | 9, 19 | imbitrrid 245 |
. . . . . . . 8
β’ (((Fun
πΆ β§ recs(πΉ) β πΆ) β§ (dom recs(πΉ) β On β§ π΅ β dom recs(πΉ))) β (π΅ β dom recs(πΉ) β (πΆβπ΅) = (πΉβ(πΆ βΎ π΅)))) |
21 | 8, 20 | mpanl2 698 |
. . . . . . 7
β’ ((Fun
πΆ β§ (dom recs(πΉ) β On β§ π΅ β dom recs(πΉ))) β (π΅ β dom recs(πΉ) β (πΆβπ΅) = (πΉβ(πΆ βΎ π΅)))) |
22 | 6, 21 | sylan 579 |
. . . . . 6
β’ ((dom
recs(πΉ) β On β§
(dom recs(πΉ) β On
β§ π΅ β dom
recs(πΉ))) β (π΅ β dom recs(πΉ) β (πΆβπ΅) = (πΉβ(πΆ βΎ π΅)))) |
23 | 22 | exp32 420 |
. . . . 5
β’ (dom
recs(πΉ) β On β
(dom recs(πΉ) β On
β (π΅ β dom
recs(πΉ) β (π΅ β dom recs(πΉ) β (πΆβπ΅) = (πΉβ(πΆ βΎ π΅)))))) |
24 | 23 | pm2.43i 52 |
. . . 4
β’ (dom
recs(πΉ) β On β
(π΅ β dom recs(πΉ) β (π΅ β dom recs(πΉ) β (πΆβπ΅) = (πΉβ(πΆ βΎ π΅))))) |
25 | 24 | pm2.43d 53 |
. . 3
β’ (dom
recs(πΉ) β On β
(π΅ β dom recs(πΉ) β (πΆβπ΅) = (πΉβ(πΆ βΎ π΅)))) |
26 | | opex 5464 |
. . . . . . . . 9
β’
β¨π΅, (πΉβ(πΆ βΎ π΅))β© β V |
27 | 26 | snid 4664 |
. . . . . . . 8
β’
β¨π΅, (πΉβ(πΆ βΎ π΅))β© β {β¨π΅, (πΉβ(πΆ βΎ π΅))β©} |
28 | | opeq1 4873 |
. . . . . . . . . . 11
β’ (π΅ = dom recs(πΉ) β β¨π΅, (πΉβ(πΆ βΎ π΅))β© = β¨dom recs(πΉ), (πΉβ(πΆ βΎ π΅))β©) |
29 | 28 | adantl 481 |
. . . . . . . . . 10
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β β¨π΅, (πΉβ(πΆ βΎ π΅))β© = β¨dom recs(πΉ), (πΉβ(πΆ βΎ π΅))β©) |
30 | | eqimss 4040 |
. . . . . . . . . . . . . 14
β’ (π΅ = dom recs(πΉ) β π΅ β dom recs(πΉ)) |
31 | 8, 15 | mp3an2 1448 |
. . . . . . . . . . . . . 14
β’ ((Fun
πΆ β§ π΅ β dom recs(πΉ)) β (πΆ βΎ π΅) = (recs(πΉ) βΎ π΅)) |
32 | 6, 30, 31 | syl2an 595 |
. . . . . . . . . . . . 13
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β (πΆ βΎ π΅) = (recs(πΉ) βΎ π΅)) |
33 | | reseq2 5976 |
. . . . . . . . . . . . . . 15
β’ (π΅ = dom recs(πΉ) β (recs(πΉ) βΎ π΅) = (recs(πΉ) βΎ dom recs(πΉ))) |
34 | 2 | tfrlem6 8385 |
. . . . . . . . . . . . . . . 16
β’ Rel
recs(πΉ) |
35 | | resdm 6026 |
. . . . . . . . . . . . . . . 16
β’ (Rel
recs(πΉ) β (recs(πΉ) βΎ dom recs(πΉ)) = recs(πΉ)) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
(recs(πΉ) βΎ dom
recs(πΉ)) = recs(πΉ) |
37 | 33, 36 | eqtrdi 2787 |
. . . . . . . . . . . . . 14
β’ (π΅ = dom recs(πΉ) β (recs(πΉ) βΎ π΅) = recs(πΉ)) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . 13
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β (recs(πΉ) βΎ π΅) = recs(πΉ)) |
39 | 32, 38 | eqtrd 2771 |
. . . . . . . . . . . 12
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β (πΆ βΎ π΅) = recs(πΉ)) |
40 | 39 | fveq2d 6895 |
. . . . . . . . . . 11
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β (πΉβ(πΆ βΎ π΅)) = (πΉβrecs(πΉ))) |
41 | 40 | opeq2d 4880 |
. . . . . . . . . 10
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β β¨dom recs(πΉ), (πΉβ(πΆ βΎ π΅))β© = β¨dom recs(πΉ), (πΉβrecs(πΉ))β©) |
42 | 29, 41 | eqtrd 2771 |
. . . . . . . . 9
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β β¨π΅, (πΉβ(πΆ βΎ π΅))β© = β¨dom recs(πΉ), (πΉβrecs(πΉ))β©) |
43 | 42 | sneqd 4640 |
. . . . . . . 8
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β {β¨π΅, (πΉβ(πΆ βΎ π΅))β©} = {β¨dom recs(πΉ), (πΉβrecs(πΉ))β©}) |
44 | 27, 43 | eleqtrid 2838 |
. . . . . . 7
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β β¨π΅, (πΉβ(πΆ βΎ π΅))β© β {β¨dom recs(πΉ), (πΉβrecs(πΉ))β©}) |
45 | | elun2 4177 |
. . . . . . 7
β’
(β¨π΅, (πΉβ(πΆ βΎ π΅))β© β {β¨dom recs(πΉ), (πΉβrecs(πΉ))β©} β β¨π΅, (πΉβ(πΆ βΎ π΅))β© β (recs(πΉ) βͺ {β¨dom recs(πΉ), (πΉβrecs(πΉ))β©})) |
46 | 44, 45 | syl 17 |
. . . . . 6
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β β¨π΅, (πΉβ(πΆ βΎ π΅))β© β (recs(πΉ) βͺ {β¨dom recs(πΉ), (πΉβrecs(πΉ))β©})) |
47 | 46, 3 | eleqtrrdi 2843 |
. . . . 5
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β β¨π΅, (πΉβ(πΆ βΎ π΅))β© β πΆ) |
48 | | simpr 484 |
. . . . . . 7
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β π΅ = dom recs(πΉ)) |
49 | | sucidg 6445 |
. . . . . . . 8
β’ (dom
recs(πΉ) β On β
dom recs(πΉ) β suc dom
recs(πΉ)) |
50 | 49 | adantr 480 |
. . . . . . 7
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β dom recs(πΉ) β suc dom recs(πΉ)) |
51 | 48, 50 | eqeltrd 2832 |
. . . . . 6
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β π΅ β suc dom recs(πΉ)) |
52 | | fnopfvb 6945 |
. . . . . 6
β’ ((πΆ Fn suc dom recs(πΉ) β§ π΅ β suc dom recs(πΉ)) β ((πΆβπ΅) = (πΉβ(πΆ βΎ π΅)) β β¨π΅, (πΉβ(πΆ βΎ π΅))β© β πΆ)) |
53 | 4, 51, 52 | syl2an2r 682 |
. . . . 5
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β ((πΆβπ΅) = (πΉβ(πΆ βΎ π΅)) β β¨π΅, (πΉβ(πΆ βΎ π΅))β© β πΆ)) |
54 | 47, 53 | mpbird 257 |
. . . 4
β’ ((dom
recs(πΉ) β On β§
π΅ = dom recs(πΉ)) β (πΆβπ΅) = (πΉβ(πΆ βΎ π΅))) |
55 | 54 | ex 412 |
. . 3
β’ (dom
recs(πΉ) β On β
(π΅ = dom recs(πΉ) β (πΆβπ΅) = (πΉβ(πΆ βΎ π΅)))) |
56 | 25, 55 | jaod 856 |
. 2
β’ (dom
recs(πΉ) β On β
((π΅ β dom recs(πΉ) β¨ π΅ = dom recs(πΉ)) β (πΆβπ΅) = (πΉβ(πΆ βΎ π΅)))) |
57 | 1, 56 | syl5 34 |
1
β’ (dom
recs(πΉ) β On β
(π΅ β suc dom
recs(πΉ) β (πΆβπ΅) = (πΉβ(πΆ βΎ π΅)))) |