Step | Hyp | Ref
| Expression |
1 | | r19.26 3111 |
. . . 4
β’
(βπ β
(β€β₯βπ)(π β§ π) β (βπ β (β€β₯βπ)π β§ βπ β (β€β₯βπ)π)) |
2 | 1 | rexbii 3094 |
. . 3
β’
(βπ β
β€ βπ β
(β€β₯βπ)(π β§ π) β βπ β β€ (βπ β (β€β₯βπ)π β§ βπ β (β€β₯βπ)π)) |
3 | | r19.40 3119 |
. . 3
β’
(βπ β
β€ (βπ β
(β€β₯βπ)π β§ βπ β (β€β₯βπ)π) β (βπ β β€ βπ β (β€β₯βπ)π β§ βπ β β€ βπ β (β€β₯βπ)π)) |
4 | 2, 3 | sylbi 216 |
. 2
β’
(βπ β
β€ βπ β
(β€β₯βπ)(π β§ π) β (βπ β β€ βπ β (β€β₯βπ)π β§ βπ β β€ βπ β (β€β₯βπ)π)) |
5 | | uzf 12774 |
. . . 4
β’
β€β₯:β€βΆπ« β€ |
6 | | ffn 6672 |
. . . 4
β’
(β€β₯:β€βΆπ« β€ β
β€β₯ Fn β€) |
7 | | raleq 3308 |
. . . . 5
β’ (π₯ =
(β€β₯βπ) β (βπ β π₯ π β βπ β (β€β₯βπ)π)) |
8 | 7 | rexrn 7041 |
. . . 4
β’
(β€β₯ Fn β€ β (βπ₯ β ran
β€β₯βπ β π₯ π β βπ β β€ βπ β (β€β₯βπ)π)) |
9 | 5, 6, 8 | mp2b 10 |
. . 3
β’
(βπ₯ β ran
β€β₯βπ β π₯ π β βπ β β€ βπ β (β€β₯βπ)π) |
10 | | raleq 3308 |
. . . . 5
β’ (π¦ =
(β€β₯βπ) β (βπ β π¦ π β βπ β (β€β₯βπ)π)) |
11 | 10 | rexrn 7041 |
. . . 4
β’
(β€β₯ Fn β€ β (βπ¦ β ran
β€β₯βπ β π¦ π β βπ β β€ βπ β (β€β₯βπ)π)) |
12 | 5, 6, 11 | mp2b 10 |
. . 3
β’
(βπ¦ β ran
β€β₯βπ β π¦ π β βπ β β€ βπ β (β€β₯βπ)π) |
13 | | uzin2 15238 |
. . . . . . . . 9
β’ ((π₯ β ran
β€β₯ β§ π¦ β ran β€β₯) β
(π₯ β© π¦) β ran
β€β₯) |
14 | | inss1 4192 |
. . . . . . . . . . . 12
β’ (π₯ β© π¦) β π₯ |
15 | | ssralv 4014 |
. . . . . . . . . . . 12
β’ ((π₯ β© π¦) β π₯ β (βπ β π₯ π β βπ β (π₯ β© π¦)π)) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . 11
β’
(βπ β
π₯ π β βπ β (π₯ β© π¦)π) |
17 | | inss2 4193 |
. . . . . . . . . . . 12
β’ (π₯ β© π¦) β π¦ |
18 | | ssralv 4014 |
. . . . . . . . . . . 12
β’ ((π₯ β© π¦) β π¦ β (βπ β π¦ π β βπ β (π₯ β© π¦)π)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . 11
β’
(βπ β
π¦ π β βπ β (π₯ β© π¦)π) |
20 | 16, 19 | anim12i 614 |
. . . . . . . . . 10
β’
((βπ β
π₯ π β§ βπ β π¦ π) β (βπ β (π₯ β© π¦)π β§ βπ β (π₯ β© π¦)π)) |
21 | | r19.26 3111 |
. . . . . . . . . 10
β’
(βπ β
(π₯ β© π¦)(π β§ π) β (βπ β (π₯ β© π¦)π β§ βπ β (π₯ β© π¦)π)) |
22 | 20, 21 | sylibr 233 |
. . . . . . . . 9
β’
((βπ β
π₯ π β§ βπ β π¦ π) β βπ β (π₯ β© π¦)(π β§ π)) |
23 | | raleq 3308 |
. . . . . . . . . 10
β’ (π§ = (π₯ β© π¦) β (βπ β π§ (π β§ π) β βπ β (π₯ β© π¦)(π β§ π))) |
24 | 23 | rspcev 3583 |
. . . . . . . . 9
β’ (((π₯ β© π¦) β ran β€β₯ β§
βπ β (π₯ β© π¦)(π β§ π)) β βπ§ β ran
β€β₯βπ β π§ (π β§ π)) |
25 | 13, 22, 24 | syl2an 597 |
. . . . . . . 8
β’ (((π₯ β ran
β€β₯ β§ π¦ β ran β€β₯) β§
(βπ β π₯ π β§ βπ β π¦ π)) β βπ§ β ran
β€β₯βπ β π§ (π β§ π)) |
26 | 25 | an4s 659 |
. . . . . . 7
β’ (((π₯ β ran
β€β₯ β§ βπ β π₯ π) β§ (π¦ β ran β€β₯ β§
βπ β π¦ π)) β βπ§ β ran
β€β₯βπ β π§ (π β§ π)) |
27 | 26 | rexlimdvaa 3150 |
. . . . . 6
β’ ((π₯ β ran
β€β₯ β§ βπ β π₯ π) β (βπ¦ β ran
β€β₯βπ β π¦ π β βπ§ β ran
β€β₯βπ β π§ (π β§ π))) |
28 | 27 | rexlimiva 3141 |
. . . . 5
β’
(βπ₯ β ran
β€β₯βπ β π₯ π β (βπ¦ β ran
β€β₯βπ β π¦ π β βπ§ β ran
β€β₯βπ β π§ (π β§ π))) |
29 | 28 | imp 408 |
. . . 4
β’
((βπ₯ β
ran β€β₯βπ β π₯ π β§ βπ¦ β ran
β€β₯βπ β π¦ π) β βπ§ β ran
β€β₯βπ β π§ (π β§ π)) |
30 | | raleq 3308 |
. . . . . 6
β’ (π§ =
(β€β₯βπ) β (βπ β π§ (π β§ π) β βπ β (β€β₯βπ)(π β§ π))) |
31 | 30 | rexrn 7041 |
. . . . 5
β’
(β€β₯ Fn β€ β (βπ§ β ran
β€β₯βπ β π§ (π β§ π) β βπ β β€ βπ β (β€β₯βπ)(π β§ π))) |
32 | 5, 6, 31 | mp2b 10 |
. . . 4
β’
(βπ§ β ran
β€β₯βπ β π§ (π β§ π) β βπ β β€ βπ β (β€β₯βπ)(π β§ π)) |
33 | 29, 32 | sylib 217 |
. . 3
β’
((βπ₯ β
ran β€β₯βπ β π₯ π β§ βπ¦ β ran
β€β₯βπ β π¦ π) β βπ β β€ βπ β (β€β₯βπ)(π β§ π)) |
34 | 9, 12, 33 | syl2anbr 600 |
. 2
β’
((βπ β
β€ βπ β
(β€β₯βπ)π β§ βπ β β€ βπ β (β€β₯βπ)π) β βπ β β€ βπ β (β€β₯βπ)(π β§ π)) |
35 | 4, 34 | impbii 208 |
1
β’
(βπ β
β€ βπ β
(β€β₯βπ)(π β§ π) β (βπ β β€ βπ β (β€β₯βπ)π β§ βπ β β€ βπ β (β€β₯βπ)π)) |