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	⊢ ( 𝜑 → ≤ ⊆ ( 𝐵 × 𝐵 ) )