Metamath Proof Explorer


Theorem prsssdm

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

Ref Expression
Hypotheses ordtNEW.b 𝐵 = ( Base ‘ 𝐾 )
ordtNEW.l = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
Assertion prsssdm ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → dom ( ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 ordtNEW.b 𝐵 = ( Base ‘ 𝐾 )
2 ordtNEW.l = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3 1 2 prsss ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → ( ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) )
4 3 dmeqd ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → dom ( ∩ ( 𝐴 × 𝐴 ) ) = dom ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) )
5 1 ressprs ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → ( 𝐾s 𝐴 ) ∈ Proset )
6 eqid ( Base ‘ ( 𝐾s 𝐴 ) ) = ( Base ‘ ( 𝐾s 𝐴 ) )
7 eqid ( ( le ‘ ( 𝐾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾s 𝐴 ) ) × ( Base ‘ ( 𝐾s 𝐴 ) ) ) ) = ( ( le ‘ ( 𝐾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾s 𝐴 ) ) × ( Base ‘ ( 𝐾s 𝐴 ) ) ) )
8 6 7 prsdm ( ( 𝐾s 𝐴 ) ∈ Proset → dom ( ( le ‘ ( 𝐾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾s 𝐴 ) ) × ( Base ‘ ( 𝐾s 𝐴 ) ) ) ) = ( Base ‘ ( 𝐾s 𝐴 ) ) )
9 5 8 syl ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → dom ( ( le ‘ ( 𝐾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾s 𝐴 ) ) × ( Base ‘ ( 𝐾s 𝐴 ) ) ) ) = ( Base ‘ ( 𝐾s 𝐴 ) ) )
10 eqid ( 𝐾s 𝐴 ) = ( 𝐾s 𝐴 )
11 10 1 ressbas2 ( 𝐴𝐵𝐴 = ( Base ‘ ( 𝐾s 𝐴 ) ) )
12 fvex ( Base ‘ ( 𝐾s 𝐴 ) ) ∈ V
13 11 12 eqeltrdi ( 𝐴𝐵𝐴 ∈ V )
14 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
15 10 14 ressle ( 𝐴 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾s 𝐴 ) ) )
16 13 15 syl ( 𝐴𝐵 → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾s 𝐴 ) ) )
17 16 adantl ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾s 𝐴 ) ) )
18 11 adantl ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → 𝐴 = ( Base ‘ ( 𝐾s 𝐴 ) ) )
19 18 sqxpeqd ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → ( 𝐴 × 𝐴 ) = ( ( Base ‘ ( 𝐾s 𝐴 ) ) × ( Base ‘ ( 𝐾s 𝐴 ) ) ) )
20 17 19 ineq12d ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ ( 𝐾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾s 𝐴 ) ) × ( Base ‘ ( 𝐾s 𝐴 ) ) ) ) )
21 20 dmeqd ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → dom ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) = dom ( ( le ‘ ( 𝐾s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾s 𝐴 ) ) × ( Base ‘ ( 𝐾s 𝐴 ) ) ) ) )
22 9 21 18 3eqtr4d ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → dom ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
23 4 22 eqtrd ( ( 𝐾 ∈ Proset ∧ 𝐴𝐵 ) → dom ( ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )