Metamath Proof Explorer

Theorem prsssdm

Description: Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-Sep-2018)

Ref Expression
Hypotheses ordtNEW.b 
|- B = ( Base ` K )
ordtNEW.l 
|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
Assertion prsssdm 
|- ( ( K e. Proset /\ A C_ B ) -> dom ( .<_ i^i ( A X. A ) ) = A )

Proof

Step Hyp Ref Expression
1 ordtNEW.b 
 |-  B = ( Base ` K )
2 ordtNEW.l 
 |-  .<_ = ( ( le ` K ) i^i ( B X. B ) )
3 1 2 prsss 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( .<_ i^i ( A X. A ) ) = ( ( le ` K ) i^i ( A X. A ) ) )
4 3 dmeqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( .<_ i^i ( A X. A ) ) = dom ( ( le ` K ) i^i ( A X. A ) ) )
5 1 ressprs 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( K |`s A ) e. Proset )
6 eqid 
 |-  ( Base ` ( K |`s A ) ) = ( Base ` ( K |`s A ) )
7 eqid 
 |-  ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) = ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) )
8 6 7 prsdm 
 |-  ( ( K |`s A ) e. Proset -> dom ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) = ( Base ` ( K |`s A ) ) )
9 5 8 syl 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) = ( Base ` ( K |`s A ) ) )
10 eqid 
 |-  ( K |`s A ) = ( K |`s A )
11 10 1 ressbas2 
 |-  ( A C_ B -> A = ( Base ` ( K |`s A ) ) )
12 fvex 
 |-  ( Base ` ( K |`s A ) ) e. _V
13 11 12 eqeltrdi 
 |-  ( A C_ B -> A e. _V )
14 eqid 
 |-  ( le ` K ) = ( le ` K )
15 10 14 ressle 
 |-  ( A e. _V -> ( le ` K ) = ( le ` ( K |`s A ) ) )
16 13 15 syl 
 |-  ( A C_ B -> ( le ` K ) = ( le ` ( K |`s A ) ) )
17 16 adantl 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( le ` K ) = ( le ` ( K |`s A ) ) )
18 11 adantl 
 |-  ( ( K e. Proset /\ A C_ B ) -> A = ( Base ` ( K |`s A ) ) )
19 18 sqxpeqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( A X. A ) = ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) )
20 17 19 ineq12d 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ( le ` K ) i^i ( A X. A ) ) = ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
21 20 dmeqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( ( le ` K ) i^i ( A X. A ) ) = dom ( ( le ` ( K |`s A ) ) i^i ( ( Base ` ( K |`s A ) ) X. ( Base ` ( K |`s A ) ) ) ) )
22 9 21 18 3eqtr4d 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( ( le ` K ) i^i ( A X. A ) ) = A )
23 4 22 eqtrd 
 |-  ( ( K e. Proset /\ A C_ B ) -> dom ( .<_ i^i ( A X. A ) ) = A )