Step | Hyp | Ref
| Expression |
1 | | iccf 13390 |
. . . . . 6
β’
[,]:(β* Γ β*)βΆπ«
β* |
2 | | inss2 4209 |
. . . . . . . 8
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
3 | | rexpssxrxp 11224 |
. . . . . . . 8
β’ (β
Γ β) β (β* Γ
β*) |
4 | 2, 3 | sstri 3971 |
. . . . . . 7
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
5 | | fss 6705 |
. . . . . . 7
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΉ:ββΆ(β* Γ
β*)) |
6 | 4, 5 | mpan2 689 |
. . . . . 6
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β πΉ:ββΆ(β* Γ
β*)) |
7 | | fco 6712 |
. . . . . 6
β’
(([,]:(β* Γ β*)βΆπ«
β* β§ πΉ:ββΆ(β* Γ
β*)) β ([,] β πΉ):ββΆπ«
β*) |
8 | 1, 6, 7 | sylancr 587 |
. . . . 5
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β ([,] β πΉ):ββΆπ«
β*) |
9 | | ffn 6688 |
. . . . 5
β’ (([,]
β πΉ):ββΆπ«
β* β ([,] β πΉ) Fn β) |
10 | | fniunfv 7214 |
. . . . 5
β’ (([,]
β πΉ) Fn β
β βͺ π β β (([,] β πΉ)βπ) = βͺ ran ([,]
β πΉ)) |
11 | 8, 9, 10 | 3syl 18 |
. . . 4
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β βͺ π β β (([,] β
πΉ)βπ) = βͺ ran ([,]
β πΉ)) |
12 | 11 | sseq2d 3994 |
. . 3
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β (π΄ β βͺ
π β β (([,]
β πΉ)βπ) β π΄ β βͺ ran
([,] β πΉ))) |
13 | 12 | adantl 482 |
. 2
β’ ((π΄ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β (π΄ β βͺ
π β β (([,]
β πΉ)βπ) β π΄ β βͺ ran
([,] β πΉ))) |
14 | | dfss3 3950 |
. . 3
β’ (π΄ β βͺ π β β (([,] β πΉ)βπ) β βπ§ β π΄ π§ β βͺ
π β β (([,]
β πΉ)βπ)) |
15 | | ssel2 3957 |
. . . . . 6
β’ ((π΄ β β β§ π§ β π΄) β π§ β β) |
16 | | eliun 4978 |
. . . . . . 7
β’ (π§ β βͺ π β β (([,] β πΉ)βπ) β βπ β β π§ β (([,] β πΉ)βπ)) |
17 | | simpll 765 |
. . . . . . . . 9
β’ (((π§ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β§ π β β) β π§ β β) |
18 | | fvco3 6960 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (([,] β πΉ)βπ) = ([,]β(πΉβπ))) |
19 | | ffvelcdm 7052 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΉβπ) β ( β€ β© (β Γ
β))) |
20 | 19 | elin2d 4179 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΉβπ) β (β Γ
β)) |
21 | | 1st2nd2 7980 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β (β Γ β) β
(πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
23 | 22 | fveq2d 6866 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ([,]β(πΉβπ)) = ([,]ββ¨(1st
β(πΉβπ)), (2nd
β(πΉβπ))β©)) |
24 | | df-ov 7380 |
. . . . . . . . . . . . . 14
β’
((1st β(πΉβπ))[,](2nd β(πΉβπ))) = ([,]ββ¨(1st
β(πΉβπ)), (2nd
β(πΉβπ))β©) |
25 | 23, 24 | eqtr4di 2789 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ([,]β(πΉβπ)) = ((1st β(πΉβπ))[,](2nd β(πΉβπ)))) |
26 | 18, 25 | eqtrd 2771 |
. . . . . . . . . . . 12
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (([,] β πΉ)βπ) = ((1st β(πΉβπ))[,](2nd β(πΉβπ)))) |
27 | 26 | eleq2d 2818 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (π§ β (([,] β πΉ)βπ) β π§ β ((1st β(πΉβπ))[,](2nd β(πΉβπ))))) |
28 | | ovolfcl 24882 |
. . . . . . . . . . . 12
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ((1st
β(πΉβπ)) β β β§
(2nd β(πΉβπ)) β β β§ (1st
β(πΉβπ)) β€ (2nd
β(πΉβπ)))) |
29 | | elicc2 13354 |
. . . . . . . . . . . . . 14
β’
(((1st β(πΉβπ)) β β β§ (2nd
β(πΉβπ)) β β) β (π§ β ((1st
β(πΉβπ))[,](2nd
β(πΉβπ))) β (π§ β β β§ (1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) |
30 | | 3anass 1095 |
. . . . . . . . . . . . . 14
β’ ((π§ β β β§
(1st β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))) β (π§ β β β§ ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) |
31 | 29, 30 | bitrdi 286 |
. . . . . . . . . . . . 13
β’
(((1st β(πΉβπ)) β β β§ (2nd
β(πΉβπ)) β β) β (π§ β ((1st
β(πΉβπ))[,](2nd
β(πΉβπ))) β (π§ β β β§ ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ)))))) |
32 | 31 | 3adant3 1132 |
. . . . . . . . . . . 12
β’
(((1st β(πΉβπ)) β β β§ (2nd
β(πΉβπ)) β β β§
(1st β(πΉβπ)) β€ (2nd β(πΉβπ))) β (π§ β ((1st β(πΉβπ))[,](2nd β(πΉβπ))) β (π§ β β β§ ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ)))))) |
33 | 28, 32 | syl 17 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (π§ β ((1st β(πΉβπ))[,](2nd β(πΉβπ))) β (π§ β β β§ ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ)))))) |
34 | 27, 33 | bitrd 278 |
. . . . . . . . . 10
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (π§ β (([,] β πΉ)βπ) β (π§ β β β§ ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ)))))) |
35 | 34 | adantll 712 |
. . . . . . . . 9
β’ (((π§ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β§ π β β) β (π§ β (([,] β πΉ)βπ) β (π§ β β β§ ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ)))))) |
36 | 17, 35 | mpbirand 705 |
. . . . . . . 8
β’ (((π§ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β§ π β β) β (π§ β (([,] β πΉ)βπ) β ((1st β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) |
37 | 36 | rexbidva 3175 |
. . . . . . 7
β’ ((π§ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β (βπ β β π§ β (([,] β πΉ)βπ) β βπ β β ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) |
38 | 16, 37 | bitrid 282 |
. . . . . 6
β’ ((π§ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β (π§ β βͺ
π β β (([,]
β πΉ)βπ) β βπ β β ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) |
39 | 15, 38 | sylan 580 |
. . . . 5
β’ (((π΄ β β β§ π§ β π΄) β§ πΉ:ββΆ( β€ β© (β
Γ β))) β (π§ β βͺ
π β β (([,]
β πΉ)βπ) β βπ β β ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) |
40 | 39 | an32s 650 |
. . . 4
β’ (((π΄ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β§ π§ β π΄) β (π§ β βͺ
π β β (([,]
β πΉ)βπ) β βπ β β ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) |
41 | 40 | ralbidva 3174 |
. . 3
β’ ((π΄ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β (βπ§ β π΄ π§ β βͺ
π β β (([,]
β πΉ)βπ) β βπ§ β π΄ βπ β β ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) |
42 | 14, 41 | bitrid 282 |
. 2
β’ ((π΄ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β (π΄ β βͺ
π β β (([,]
β πΉ)βπ) β βπ§ β π΄ βπ β β ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) |
43 | 13, 42 | bitr3d 280 |
1
β’ ((π΄ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β (π΄ β βͺ ran
([,] β πΉ) β
βπ§ β π΄ βπ β β ((1st
β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) |