This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imasless

Description: The order relation defined on an image set is a subset of the base set. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasless.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasless.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasless.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imasless.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
imasless.l ⊢ ≤ = ( le ‘ 𝑈 )
Assertion imasless ( 𝜑 → ≤ ⊆ ( 𝐵 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 imasless.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasless.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasless.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4 imasless.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5 imasless.l ⊢ ≤ = ( le ‘ 𝑈 )
6 eqid ⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
7 1 2 3 4 6 5 imasle ⊢ ( 𝜑 → ≤ = ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) )
8 relco ⊢ Rel ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 )
9 relssdmrn ⊢ ( Rel ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) → ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⊆ ( dom ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) × ran ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ) )
10 8 9 ax-mp ⊢ ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⊆ ( dom ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) × ran ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) )
11 dmco ⊢ dom ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) = ( ◡ ◡ 𝐹 “ dom ( 𝐹 ∘ ( le ‘ 𝑅 ) ) )
12 fof ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 : 𝑉 ⟶ 𝐵 )
13 frel ⊢ ( 𝐹 : 𝑉 ⟶ 𝐵 → Rel 𝐹 )
14 3 12 13 3syl ⊢ ( 𝜑 → Rel 𝐹 )
15 dfrel2 ⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
16 14 15 sylib ⊢ ( 𝜑 → ◡ ◡ 𝐹 = 𝐹 )
17 16 imaeq1d ⊢ ( 𝜑 → ( ◡ ◡ 𝐹 “ dom ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ) = ( 𝐹 “ dom ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ) )
18 imassrn ⊢ ( 𝐹 “ dom ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ) ⊆ ran 𝐹
19 forn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
20 3 19 syl ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
21 18 20 sseqtrid ⊢ ( 𝜑 → ( 𝐹 “ dom ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ) ⊆ 𝐵 )
22 17 21 eqsstrd ⊢ ( 𝜑 → ( ◡ ◡ 𝐹 “ dom ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ) ⊆ 𝐵 )
23 11 22 eqsstrid ⊢ ( 𝜑 → dom ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⊆ 𝐵 )
24 rncoss ⊢ ran ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⊆ ran ( 𝐹 ∘ ( le ‘ 𝑅 ) )
25 rnco2 ⊢ ran ( 𝐹 ∘ ( le ‘ 𝑅 ) ) = ( 𝐹 “ ran ( le ‘ 𝑅 ) )
26 imassrn ⊢ ( 𝐹 “ ran ( le ‘ 𝑅 ) ) ⊆ ran 𝐹
27 26 20 sseqtrid ⊢ ( 𝜑 → ( 𝐹 “ ran ( le ‘ 𝑅 ) ) ⊆ 𝐵 )
28 25 27 eqsstrid ⊢ ( 𝜑 → ran ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ⊆ 𝐵 )
29 24 28 sstrid ⊢ ( 𝜑 → ran ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⊆ 𝐵 )
30 xpss12 ⊢ ( ( dom ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⊆ 𝐵 ∧ ran ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⊆ 𝐵 ) → ( dom ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) × ran ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ) ⊆ ( 𝐵 × 𝐵 ) )
31 23 29 30 syl2anc ⊢ ( 𝜑 → ( dom ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) × ran ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ) ⊆ ( 𝐵 × 𝐵 ) )
32 10 31 sstrid ⊢ ( 𝜑 → ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⊆ ( 𝐵 × 𝐵 ) )
33 7 32 eqsstrd ⊢ ( 𝜑 → ≤ ⊆ ( 𝐵 × 𝐵 ) )