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	$⊢ φ \to U = F “_{𝑠} R$
	imasless.v	$⊢ φ \to V = {Base}_{R}$
	imasless.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasless.r	$⊢ φ \to R \in Z$
	imasless.l	$⊢ \underset{˙}{\leq} = \leq_{U}$
Assertion	imasless	$⊢ φ \to \underset{˙}{\leq} \subseteq B \times B$

Proof

Step	Hyp	Ref	Expression
1		imasless.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasless.v	$⊢ φ \to V = {Base}_{R}$
3		imasless.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
4		imasless.r	$⊢ φ \to R \in Z$
5		imasless.l	$⊢ \underset{˙}{\leq} = \leq_{U}$
6		eqid	$⊢ \leq_{R} = \leq_{R}$
7	1 2 3 4 6 5	imasle	$⊢ φ \to \underset{˙}{\leq} = (F \circ \leq_{R}) \circ F^{-1}$
8		relco	$⊢ Rel ((F \circ \leq_{R}) \circ F^{-1})$
9		relssdmrn	$⊢ Rel ((F \circ \leq_{R}) \circ F^{-1}) \to (F \circ \leq_{R}) \circ F^{-1} \subseteq dom ((F \circ \leq_{R}) \circ F^{-1}) \times ran ((F \circ \leq_{R}) \circ F^{-1})$
10	8 9	ax-mp	$⊢ (F \circ \leq_{R}) \circ F^{-1} \subseteq dom ((F \circ \leq_{R}) \circ F^{-1}) \times ran ((F \circ \leq_{R}) \circ F^{-1})$
11		dmco	$⊢ dom ((F \circ \leq_{R}) \circ F^{-1}) = {F^{-1}}^{-1} [dom (F \circ \leq_{R})]$
12		fof	$⊢ F : V \underset{onto}{⟶} B \to F : V ⟶ B$
13		frel	$⊢ F : V ⟶ B \to Rel F$
14	3 12 13	3syl	$⊢ φ \to Rel F$
15		dfrel2	$⊢ Rel F \leftrightarrow {F^{-1}}^{-1} = F$
16	14 15	sylib	$⊢ φ \to {F^{-1}}^{-1} = F$
17	16	imaeq1d	$⊢ φ \to {F^{-1}}^{-1} [dom (F \circ \leq_{R})] = F [dom (F \circ \leq_{R})]$
18		imassrn	$⊢ F [dom (F \circ \leq_{R})] \subseteq ran F$
19		forn	$⊢ F : V \underset{onto}{⟶} B \to ran F = B$
20	3 19	syl	$⊢ φ \to ran F = B$
21	18 20	sseqtrid	$⊢ φ \to F [dom (F \circ \leq_{R})] \subseteq B$
22	17 21	eqsstrd	$⊢ φ \to {F^{-1}}^{-1} [dom (F \circ \leq_{R})] \subseteq B$
23	11 22	eqsstrid	$⊢ φ \to dom ((F \circ \leq_{R}) \circ F^{-1}) \subseteq B$
24		rncoss	$⊢ ran ((F \circ \leq_{R}) \circ F^{-1}) \subseteq ran (F \circ \leq_{R})$
25		rnco2	$⊢ ran (F \circ \leq_{R}) = F [ran \leq_{R}]$
26		imassrn	$⊢ F [ran \leq_{R}] \subseteq ran F$
27	26 20	sseqtrid	$⊢ φ \to F [ran \leq_{R}] \subseteq B$
28	25 27	eqsstrid	$⊢ φ \to ran (F \circ \leq_{R}) \subseteq B$
29	24 28	sstrid	$⊢ φ \to ran ((F \circ \leq_{R}) \circ F^{-1}) \subseteq B$
30		xpss12	$⊢ (dom ((F \circ \leq_{R}) \circ F^{-1}) \subseteq B \land ran ((F \circ \leq_{R}) \circ F^{-1}) \subseteq B) \to dom ((F \circ \leq_{R}) \circ F^{-1}) \times ran ((F \circ \leq_{R}) \circ F^{-1}) \subseteq B \times B$
31	23 29 30	syl2anc	$⊢ φ \to dom ((F \circ \leq_{R}) \circ F^{-1}) \times ran ((F \circ \leq_{R}) \circ F^{-1}) \subseteq B \times B$
32	10 31	sstrid	$⊢ φ \to (F \circ \leq_{R}) \circ F^{-1} \subseteq B \times B$
33	7 32	eqsstrd	$⊢ φ \to \underset{˙}{\leq} \subseteq B \times B$

Metamath Proof Explorer

Theorem imasless

Proof