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 ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )