Step | Hyp | Ref
| Expression |
1 | | inf3lem.1 |
. . . . . . . . . . 11
β’ πΊ = (π¦ β V β¦ {π€ β π₯ β£ (π€ β© π₯) β π¦}) |
2 | | inf3lem.2 |
. . . . . . . . . . 11
β’ πΉ = (rec(πΊ, β
) βΎ Ο) |
3 | | vex 3450 |
. . . . . . . . . . 11
β’ π’ β V |
4 | | vex 3450 |
. . . . . . . . . . 11
β’ π£ β V |
5 | 1, 2, 3, 4 | inf3lem5 9569 |
. . . . . . . . . 10
β’ ((π₯ β β
β§ π₯ β βͺ π₯)
β ((π’ β Ο
β§ π£ β π’) β (πΉβπ£) β (πΉβπ’))) |
6 | | dfpss2 4046 |
. . . . . . . . . . 11
β’ ((πΉβπ£) β (πΉβπ’) β ((πΉβπ£) β (πΉβπ’) β§ Β¬ (πΉβπ£) = (πΉβπ’))) |
7 | 6 | simprbi 498 |
. . . . . . . . . 10
β’ ((πΉβπ£) β (πΉβπ’) β Β¬ (πΉβπ£) = (πΉβπ’)) |
8 | 5, 7 | syl6 35 |
. . . . . . . . 9
β’ ((π₯ β β
β§ π₯ β βͺ π₯)
β ((π’ β Ο
β§ π£ β π’) β Β¬ (πΉβπ£) = (πΉβπ’))) |
9 | 8 | expdimp 454 |
. . . . . . . 8
β’ (((π₯ β β
β§ π₯ β βͺ π₯)
β§ π’ β Ο)
β (π£ β π’ β Β¬ (πΉβπ£) = (πΉβπ’))) |
10 | 9 | adantrl 715 |
. . . . . . 7
β’ (((π₯ β β
β§ π₯ β βͺ π₯)
β§ (π£ β Ο
β§ π’ β Ο))
β (π£ β π’ β Β¬ (πΉβπ£) = (πΉβπ’))) |
11 | 1, 2, 4, 3 | inf3lem5 9569 |
. . . . . . . . . 10
β’ ((π₯ β β
β§ π₯ β βͺ π₯)
β ((π£ β Ο
β§ π’ β π£) β (πΉβπ’) β (πΉβπ£))) |
12 | | dfpss2 4046 |
. . . . . . . . . . . 12
β’ ((πΉβπ’) β (πΉβπ£) β ((πΉβπ’) β (πΉβπ£) β§ Β¬ (πΉβπ’) = (πΉβπ£))) |
13 | 12 | simprbi 498 |
. . . . . . . . . . 11
β’ ((πΉβπ’) β (πΉβπ£) β Β¬ (πΉβπ’) = (πΉβπ£)) |
14 | | eqcom 2744 |
. . . . . . . . . . 11
β’ ((πΉβπ’) = (πΉβπ£) β (πΉβπ£) = (πΉβπ’)) |
15 | 13, 14 | sylnib 328 |
. . . . . . . . . 10
β’ ((πΉβπ’) β (πΉβπ£) β Β¬ (πΉβπ£) = (πΉβπ’)) |
16 | 11, 15 | syl6 35 |
. . . . . . . . 9
β’ ((π₯ β β
β§ π₯ β βͺ π₯)
β ((π£ β Ο
β§ π’ β π£) β Β¬ (πΉβπ£) = (πΉβπ’))) |
17 | 16 | expdimp 454 |
. . . . . . . 8
β’ (((π₯ β β
β§ π₯ β βͺ π₯)
β§ π£ β Ο)
β (π’ β π£ β Β¬ (πΉβπ£) = (πΉβπ’))) |
18 | 17 | adantrr 716 |
. . . . . . 7
β’ (((π₯ β β
β§ π₯ β βͺ π₯)
β§ (π£ β Ο
β§ π’ β Ο))
β (π’ β π£ β Β¬ (πΉβπ£) = (πΉβπ’))) |
19 | 10, 18 | jaod 858 |
. . . . . 6
β’ (((π₯ β β
β§ π₯ β βͺ π₯)
β§ (π£ β Ο
β§ π’ β Ο))
β ((π£ β π’ β¨ π’ β π£) β Β¬ (πΉβπ£) = (πΉβπ’))) |
20 | 19 | con2d 134 |
. . . . 5
β’ (((π₯ β β
β§ π₯ β βͺ π₯)
β§ (π£ β Ο
β§ π’ β Ο))
β ((πΉβπ£) = (πΉβπ’) β Β¬ (π£ β π’ β¨ π’ β π£))) |
21 | | nnord 7811 |
. . . . . . 7
β’ (π£ β Ο β Ord π£) |
22 | | nnord 7811 |
. . . . . . 7
β’ (π’ β Ο β Ord π’) |
23 | | ordtri3 6354 |
. . . . . . 7
β’ ((Ord
π£ β§ Ord π’) β (π£ = π’ β Β¬ (π£ β π’ β¨ π’ β π£))) |
24 | 21, 22, 23 | syl2an 597 |
. . . . . 6
β’ ((π£ β Ο β§ π’ β Ο) β (π£ = π’ β Β¬ (π£ β π’ β¨ π’ β π£))) |
25 | 24 | adantl 483 |
. . . . 5
β’ (((π₯ β β
β§ π₯ β βͺ π₯)
β§ (π£ β Ο
β§ π’ β Ο))
β (π£ = π’ β Β¬ (π£ β π’ β¨ π’ β π£))) |
26 | 20, 25 | sylibrd 259 |
. . . 4
β’ (((π₯ β β
β§ π₯ β βͺ π₯)
β§ (π£ β Ο
β§ π’ β Ο))
β ((πΉβπ£) = (πΉβπ’) β π£ = π’)) |
27 | 26 | ralrimivva 3198 |
. . 3
β’ ((π₯ β β
β§ π₯ β βͺ π₯)
β βπ£ β
Ο βπ’ β
Ο ((πΉβπ£) = (πΉβπ’) β π£ = π’)) |
28 | | frfnom 8382 |
. . . . . 6
β’
(rec(πΊ, β
)
βΎ Ο) Fn Ο |
29 | | fneq1 6594 |
. . . . . 6
β’ (πΉ = (rec(πΊ, β
) βΎ Ο) β (πΉ Fn Ο β (rec(πΊ, β
) βΎ Ο) Fn
Ο)) |
30 | 28, 29 | mpbiri 258 |
. . . . 5
β’ (πΉ = (rec(πΊ, β
) βΎ Ο) β πΉ Fn Ο) |
31 | | fvelrnb 6904 |
. . . . . . . 8
β’ (πΉ Fn Ο β (π’ β ran πΉ β βπ£ β Ο (πΉβπ£) = π’)) |
32 | | inf3lem.4 |
. . . . . . . . . . . 12
β’ π΅ β V |
33 | 1, 2, 4, 32 | inf3lemd 9564 |
. . . . . . . . . . 11
β’ (π£ β Ο β (πΉβπ£) β π₯) |
34 | | fvex 6856 |
. . . . . . . . . . . 12
β’ (πΉβπ£) β V |
35 | 34 | elpw 4565 |
. . . . . . . . . . 11
β’ ((πΉβπ£) β π« π₯ β (πΉβπ£) β π₯) |
36 | 33, 35 | sylibr 233 |
. . . . . . . . . 10
β’ (π£ β Ο β (πΉβπ£) β π« π₯) |
37 | | eleq1 2826 |
. . . . . . . . . 10
β’ ((πΉβπ£) = π’ β ((πΉβπ£) β π« π₯ β π’ β π« π₯)) |
38 | 36, 37 | syl5ibcom 244 |
. . . . . . . . 9
β’ (π£ β Ο β ((πΉβπ£) = π’ β π’ β π« π₯)) |
39 | 38 | rexlimiv 3146 |
. . . . . . . 8
β’
(βπ£ β
Ο (πΉβπ£) = π’ β π’ β π« π₯) |
40 | 31, 39 | syl6bi 253 |
. . . . . . 7
β’ (πΉ Fn Ο β (π’ β ran πΉ β π’ β π« π₯)) |
41 | 40 | ssrdv 3951 |
. . . . . 6
β’ (πΉ Fn Ο β ran πΉ β π« π₯) |
42 | 41 | ancli 550 |
. . . . 5
β’ (πΉ Fn Ο β (πΉ Fn Ο β§ ran πΉ β π« π₯)) |
43 | 2, 30, 42 | mp2b 10 |
. . . 4
β’ (πΉ Fn Ο β§ ran πΉ β π« π₯) |
44 | | df-f 6501 |
. . . 4
β’ (πΉ:ΟβΆπ« π₯ β (πΉ Fn Ο β§ ran πΉ β π« π₯)) |
45 | 43, 44 | mpbir 230 |
. . 3
β’ πΉ:ΟβΆπ« π₯ |
46 | 27, 45 | jctil 521 |
. 2
β’ ((π₯ β β
β§ π₯ β βͺ π₯)
β (πΉ:ΟβΆπ« π₯ β§ βπ£ β Ο βπ’ β Ο ((πΉβπ£) = (πΉβπ’) β π£ = π’))) |
47 | | dff13 7203 |
. 2
β’ (πΉ:Οβ1-1βπ« π₯ β (πΉ:ΟβΆπ« π₯ β§ βπ£ β Ο βπ’ β Ο ((πΉβπ£) = (πΉβπ’) β π£ = π’))) |
48 | 46, 47 | sylibr 233 |
1
β’ ((π₯ β β
β§ π₯ β βͺ π₯)
β πΉ:Οβ1-1βπ« π₯) |