Step | Hyp | Ref
| Expression |
1 | | vex 3451 |
. . . . . . . . . 10
β’ π β V |
2 | 1 | elixp 8848 |
. . . . . . . . 9
β’ (π β Xπ₯ β
π΄ π΅ β (π Fn π΄ β§ βπ₯ β π΄ (πβπ₯) β π΅)) |
3 | 2 | simprbi 498 |
. . . . . . . 8
β’ (π β Xπ₯ β
π΄ π΅ β βπ₯ β π΄ (πβπ₯) β π΅) |
4 | | ssiun2 5011 |
. . . . . . . . . 10
β’ (π₯ β π΄ β π΅ β βͺ
π₯ β π΄ π΅) |
5 | 4 | sseld 3947 |
. . . . . . . . 9
β’ (π₯ β π΄ β ((πβπ₯) β π΅ β (πβπ₯) β βͺ
π₯ β π΄ π΅)) |
6 | 5 | ralimia 3080 |
. . . . . . . 8
β’
(βπ₯ β
π΄ (πβπ₯) β π΅ β βπ₯ β π΄ (πβπ₯) β βͺ
π₯ β π΄ π΅) |
7 | 3, 6 | syl 17 |
. . . . . . 7
β’ (π β Xπ₯ β
π΄ π΅ β βπ₯ β π΄ (πβπ₯) β βͺ
π₯ β π΄ π΅) |
8 | | nfv 1918 |
. . . . . . . 8
β’
β²π¦(πβπ₯) β βͺ
π₯ β π΄ π΅ |
9 | | nfiu1 4992 |
. . . . . . . . 9
β’
β²π₯βͺ π₯ β π΄ π΅ |
10 | 9 | nfel2 2922 |
. . . . . . . 8
β’
β²π₯(πβπ¦) β βͺ
π₯ β π΄ π΅ |
11 | | fveq2 6846 |
. . . . . . . . 9
β’ (π₯ = π¦ β (πβπ₯) = (πβπ¦)) |
12 | 11 | eleq1d 2819 |
. . . . . . . 8
β’ (π₯ = π¦ β ((πβπ₯) β βͺ
π₯ β π΄ π΅ β (πβπ¦) β βͺ
π₯ β π΄ π΅)) |
13 | 8, 10, 12 | cbvralw 3288 |
. . . . . . 7
β’
(βπ₯ β
π΄ (πβπ₯) β βͺ
π₯ β π΄ π΅ β βπ¦ β π΄ (πβπ¦) β βͺ
π₯ β π΄ π΅) |
14 | 7, 13 | sylib 217 |
. . . . . 6
β’ (π β Xπ₯ β
π΄ π΅ β βπ¦ β π΄ (πβπ¦) β βͺ
π₯ β π΄ π΅) |
15 | 14 | adantl 483 |
. . . . 5
β’ (((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β§ π β Xπ₯ β π΄ π΅) β βπ¦ β π΄ (πβπ¦) β βͺ
π₯ β π΄ π΅) |
16 | 15 | ralrimiva 3140 |
. . . 4
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β βπ β X
π₯ β π΄ π΅βπ¦ β π΄ (πβπ¦) β βͺ
π₯ β π΄ π΅) |
17 | | eqid 2733 |
. . . . 5
β’ (π β Xπ₯ β
π΄ π΅, π¦ β π΄ β¦ (πβπ¦)) = (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)) |
18 | 17 | fmpo 8004 |
. . . 4
β’
(βπ β
X π₯
β π΄ π΅βπ¦ β π΄ (πβπ¦) β βͺ
π₯ β π΄ π΅ β (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)):(Xπ₯ β π΄ π΅ Γ π΄)βΆβͺ
π₯ β π΄ π΅) |
19 | 16, 18 | sylib 217 |
. . 3
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)):(Xπ₯ β π΄ π΅ Γ π΄)βΆβͺ
π₯ β π΄ π΅) |
20 | | ixpssmap2g 8871 |
. . . . . 6
β’ (βͺ π₯ β π΄ π΅ β π β Xπ₯ β π΄ π΅ β (βͺ π₯ β π΄ π΅ βm π΄)) |
21 | 20 | 3ad2ant2 1135 |
. . . . 5
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β Xπ₯ β
π΄ π΅ β (βͺ π₯ β π΄ π΅ βm π΄)) |
22 | | ovex 7394 |
. . . . . 6
β’ (βͺ π₯ β π΄ π΅ βm π΄) β V |
23 | 22 | ssex 5282 |
. . . . 5
β’ (Xπ₯ β
π΄ π΅ β (βͺ π₯ β π΄ π΅ βm π΄) β Xπ₯ β π΄ π΅ β V) |
24 | 21, 23 | syl 17 |
. . . 4
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β Xπ₯ β
π΄ π΅ β V) |
25 | | simp1 1137 |
. . . 4
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β π΄ β π) |
26 | 24, 25 | xpexd 7689 |
. . 3
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β (Xπ₯ β
π΄ π΅ Γ π΄) β V) |
27 | 19, 26 | fexd 7181 |
. 2
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)) β V) |
28 | 19 | ffnd 6673 |
. . . 4
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)) Fn (Xπ₯ β π΄ π΅ Γ π΄)) |
29 | | dffn4 6766 |
. . . 4
β’ ((π β Xπ₯ β
π΄ π΅, π¦ β π΄ β¦ (πβπ¦)) Fn (Xπ₯ β π΄ π΅ Γ π΄) β (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)):(Xπ₯ β π΄ π΅ Γ π΄)βontoβran (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦))) |
30 | 28, 29 | sylib 217 |
. . 3
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)):(Xπ₯ β π΄ π΅ Γ π΄)βontoβran (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦))) |
31 | | n0 4310 |
. . . . . . . . . 10
β’ (Xπ₯ β
π΄ π΅ β β
β βπ π β Xπ₯ β π΄ π΅) |
32 | | eliun 4962 |
. . . . . . . . . . . 12
β’ (π§ β βͺ π₯ β π΄ π΅ β βπ₯ β π΄ π§ β π΅) |
33 | | nfixp1 8862 |
. . . . . . . . . . . . . 14
β’
β²π₯Xπ₯ β
π΄ π΅ |
34 | 33 | nfel2 2922 |
. . . . . . . . . . . . 13
β’
β²π₯ π β Xπ₯ β
π΄ π΅ |
35 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π₯βπ¦ β π΄ π§ = (πβπ¦) |
36 | 33, 35 | nfrexw 3295 |
. . . . . . . . . . . . 13
β’
β²π₯βπ β X
π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦) |
37 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β§ π β π΄) β π§ β π΅) |
38 | | iftrue 4496 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π₯ β if(π = π₯, π§, (πβπ)) = π§) |
39 | | csbeq1a 3873 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π β π΅ = β¦π / π₯β¦π΅) |
40 | 39 | equcoms 2024 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π₯ β π΅ = β¦π / π₯β¦π΅) |
41 | 40 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π₯ β β¦π / π₯β¦π΅ = π΅) |
42 | 38, 41 | eleq12d 2828 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π₯ β (if(π = π₯, π§, (πβπ)) β β¦π / π₯β¦π΅ β π§ β π΅)) |
43 | 37, 42 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β§ π β π΄) β (π = π₯ β if(π = π₯, π§, (πβπ)) β β¦π / π₯β¦π΅)) |
44 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ π β V |
45 | 44 | elixp 8848 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β Xπ₯ β
π΄ π΅ β (π Fn π΄ β§ βπ₯ β π΄ (πβπ₯) β π΅)) |
46 | 45 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β Xπ₯ β
π΄ π΅ β βπ₯ β π΄ (πβπ₯) β π΅) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β βπ₯ β π΄ (πβπ₯) β π΅) |
48 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(πβπ₯) β π΅ |
49 | | nfcsb1v 3884 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π₯β¦π / π₯β¦π΅ |
50 | 49 | nfel2 2922 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π₯(πβπ) β β¦π / π₯β¦π΅ |
51 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
52 | 51, 39 | eleq12d 2828 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π β ((πβπ₯) β π΅ β (πβπ) β β¦π / π₯β¦π΅)) |
53 | 48, 50, 52 | cbvralw 3288 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ₯ β
π΄ (πβπ₯) β π΅ β βπ β π΄ (πβπ) β β¦π / π₯β¦π΅) |
54 | 47, 53 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β βπ β π΄ (πβπ) β β¦π / π₯β¦π΅) |
55 | 54 | r19.21bi 3233 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β§ π β π΄) β (πβπ) β β¦π / π₯β¦π΅) |
56 | | iffalse 4499 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬
π = π₯ β if(π = π₯, π§, (πβπ)) = (πβπ)) |
57 | 56 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
π = π₯ β (if(π = π₯, π§, (πβπ)) β β¦π / π₯β¦π΅ β (πβπ) β β¦π / π₯β¦π΅)) |
58 | 55, 57 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β§ π β π΄) β (Β¬ π = π₯ β if(π = π₯, π§, (πβπ)) β β¦π / π₯β¦π΅)) |
59 | 43, 58 | pm2.61d 179 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β§ π β π΄) β if(π = π₯, π§, (πβπ)) β β¦π / π₯β¦π΅) |
60 | 59 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β βπ β π΄ if(π = π₯, π§, (πβπ)) β β¦π / π₯β¦π΅) |
61 | | ixpfn 8847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Xπ₯ β
π΄ π΅ β π Fn π΄) |
62 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β π Fn π΄) |
63 | 62 | fndmd 6611 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β dom π = π΄) |
64 | 44 | dmex 7852 |
. . . . . . . . . . . . . . . . . . 19
β’ dom π β V |
65 | 63, 64 | eqeltrrdi 2843 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β π΄ β V) |
66 | | mptelixpg 8879 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β V β ((π β π΄ β¦ if(π = π₯, π§, (πβπ))) β Xπ β π΄ β¦π / π₯β¦π΅ β βπ β π΄ if(π = π₯, π§, (πβπ)) β β¦π / π₯β¦π΅)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β ((π β π΄ β¦ if(π = π₯, π§, (πβπ))) β Xπ β π΄ β¦π / π₯β¦π΅ β βπ β π΄ if(π = π₯, π§, (πβπ)) β β¦π / π₯β¦π΅)) |
68 | 60, 67 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β (π β π΄ β¦ if(π = π₯, π§, (πβπ))) β Xπ β π΄ β¦π / π₯β¦π΅) |
69 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²ππ΅ |
70 | 69, 49, 39 | cbvixp 8858 |
. . . . . . . . . . . . . . . 16
β’ Xπ₯ β
π΄ π΅ = Xπ β π΄ β¦π / π₯β¦π΅ |
71 | 68, 70 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . 15
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β (π β π΄ β¦ if(π = π₯, π§, (πβπ))) β Xπ₯ β π΄ π΅) |
72 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β π₯ β π΄) |
73 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β¦ if(π = π₯, π§, (πβπ))) = (π β π΄ β¦ if(π = π₯, π§, (πβπ))) |
74 | | vex 3451 |
. . . . . . . . . . . . . . . . . 18
β’ π§ β V |
75 | 38, 73, 74 | fvmpt 6952 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π΄ β ((π β π΄ β¦ if(π = π₯, π§, (πβπ)))βπ₯) = π§) |
76 | 75 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β ((π β π΄ β¦ if(π = π₯, π§, (πβπ)))βπ₯) = π§) |
77 | 76 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β π§ = ((π β π΄ β¦ if(π = π₯, π§, (πβπ)))βπ₯)) |
78 | | fveq1 6845 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π β π΄ β¦ if(π = π₯, π§, (πβπ))) β (πβπ¦) = ((π β π΄ β¦ if(π = π₯, π§, (πβπ)))βπ¦)) |
79 | 78 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’ (π = (π β π΄ β¦ if(π = π₯, π§, (πβπ))) β (π§ = (πβπ¦) β π§ = ((π β π΄ β¦ if(π = π₯, π§, (πβπ)))βπ¦))) |
80 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π₯ β ((π β π΄ β¦ if(π = π₯, π§, (πβπ)))βπ¦) = ((π β π΄ β¦ if(π = π₯, π§, (πβπ)))βπ₯)) |
81 | 80 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β (π§ = ((π β π΄ β¦ if(π = π₯, π§, (πβπ)))βπ¦) β π§ = ((π β π΄ β¦ if(π = π₯, π§, (πβπ)))βπ₯))) |
82 | 79, 81 | rspc2ev 3594 |
. . . . . . . . . . . . . . 15
β’ (((π β π΄ β¦ if(π = π₯, π§, (πβπ))) β Xπ₯ β π΄ π΅ β§ π₯ β π΄ β§ π§ = ((π β π΄ β¦ if(π = π₯, π§, (πβπ)))βπ₯)) β βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦)) |
83 | 71, 72, 77, 82 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β Xπ₯ β
π΄ π΅ β§ (π₯ β π΄ β§ π§ β π΅)) β βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦)) |
84 | 83 | exp32 422 |
. . . . . . . . . . . . 13
β’ (π β Xπ₯ β
π΄ π΅ β (π₯ β π΄ β (π§ β π΅ β βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦)))) |
85 | 34, 36, 84 | rexlimd 3248 |
. . . . . . . . . . . 12
β’ (π β Xπ₯ β
π΄ π΅ β (βπ₯ β π΄ π§ β π΅ β βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦))) |
86 | 32, 85 | biimtrid 241 |
. . . . . . . . . . 11
β’ (π β Xπ₯ β
π΄ π΅ β (π§ β βͺ
π₯ β π΄ π΅ β βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦))) |
87 | 86 | exlimiv 1934 |
. . . . . . . . . 10
β’
(βπ π β Xπ₯ β
π΄ π΅ β (π§ β βͺ
π₯ β π΄ π΅ β βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦))) |
88 | 31, 87 | sylbi 216 |
. . . . . . . . 9
β’ (Xπ₯ β
π΄ π΅ β β
β (π§ β βͺ
π₯ β π΄ π΅ β βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦))) |
89 | 88 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β (π§ β βͺ
π₯ β π΄ π΅ β βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦))) |
90 | 89 | alrimiv 1931 |
. . . . . . 7
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β βπ§(π§ β βͺ
π₯ β π΄ π΅ β βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦))) |
91 | | ssab 4022 |
. . . . . . 7
β’ (βͺ π₯ β π΄ π΅ β {π§ β£ βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦)} β βπ§(π§ β βͺ
π₯ β π΄ π΅ β βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦))) |
92 | 90, 91 | sylibr 233 |
. . . . . 6
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β βͺ π₯ β π΄ π΅ β {π§ β£ βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦)}) |
93 | 17 | rnmpo 7493 |
. . . . . 6
β’ ran
(π β Xπ₯ β
π΄ π΅, π¦ β π΄ β¦ (πβπ¦)) = {π§ β£ βπ β X π₯ β π΄ π΅βπ¦ β π΄ π§ = (πβπ¦)} |
94 | 92, 93 | sseqtrrdi 3999 |
. . . . 5
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β βͺ π₯ β π΄ π΅ β ran (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦))) |
95 | 19 | frnd 6680 |
. . . . 5
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β ran (π β Xπ₯ β
π΄ π΅, π¦ β π΄ β¦ (πβπ¦)) β βͺ π₯ β π΄ π΅) |
96 | 94, 95 | eqssd 3965 |
. . . 4
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β βͺ π₯ β π΄ π΅ = ran (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦))) |
97 | | foeq3 6758 |
. . . 4
β’ (βͺ π₯ β π΄ π΅ = ran (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)) β ((π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)):(Xπ₯ β π΄ π΅ Γ π΄)βontoββͺ π₯ β π΄ π΅ β (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)):(Xπ₯ β π΄ π΅ Γ π΄)βontoβran (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)))) |
98 | 96, 97 | syl 17 |
. . 3
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β ((π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)):(Xπ₯ β π΄ π΅ Γ π΄)βontoββͺ π₯ β π΄ π΅ β (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)):(Xπ₯ β π΄ π΅ Γ π΄)βontoβran (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)))) |
99 | 30, 98 | mpbird 257 |
. 2
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)):(Xπ₯ β π΄ π΅ Γ π΄)βontoββͺ π₯ β π΄ π΅) |
100 | | fowdom 9515 |
. 2
β’ (((π β Xπ₯ β
π΄ π΅, π¦ β π΄ β¦ (πβπ¦)) β V β§ (π β Xπ₯ β π΄ π΅, π¦ β π΄ β¦ (πβπ¦)):(Xπ₯ β π΄ π΅ Γ π΄)βontoββͺ π₯ β π΄ π΅) β βͺ
π₯ β π΄ π΅ βΌ* (Xπ₯ β
π΄ π΅ Γ π΄)) |
101 | 27, 99, 100 | syl2anc 585 |
1
β’ ((π΄ β π β§ βͺ
π₯ β π΄ π΅ β π β§ Xπ₯ β π΄ π΅ β β
) β βͺ π₯ β π΄ π΅ βΌ* (Xπ₯ β
π΄ π΅ Γ π΄)) |