Theorem pmtrdifellem1

Description: Lemma 1 for pmtrdifel . (Contributed by AV, 15-Jan-2019)

	Ref	Expression
Hypotheses	pmtrdifel.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(N\setminus \left\{K\right\}\right)$$
	pmtrdifel.r	$$⊢R=\mathrm{ran}\mathrm{pmTrsp}\left(N\right)$$
	pmtrdifel.0	$$⊢S=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(Q\setminus \mathrm{I}\right)\right)$$
Assertion	pmtrdifellem1	$$⊢Q\in T\to S\in R$$

Proof

Step	Hyp	Ref	Expression
1		pmtrdifel.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(N\setminus \left\{K\right\}\right)$$
2		pmtrdifel.r	$$⊢R=\mathrm{ran}\mathrm{pmTrsp}\left(N\right)$$
3		pmtrdifel.0	$$⊢S=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(Q\setminus \mathrm{I}\right)\right)$$
4		eqid	$$⊢\mathrm{pmTrsp}\left(N\setminus \left\{K\right\}\right)=\mathrm{pmTrsp}\left(N\setminus \left\{K\right\}\right)$$
5	4 1	pmtrfb	$$⊢Q\in T\leftrightarrow \left(N\setminus \left\{K\right\}\in \mathrm{V}\wedge Q:N\setminus \left\{K\right\}\underset{1-1\; onto}{⟶}N\setminus \left\{K\right\}\wedge \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)$$
6		difsnexi	$$⊢N\setminus \left\{K\right\}\in \mathrm{V}\to N\in \mathrm{V}$$
7		f1of	$$⊢Q:N\setminus \left\{K\right\}\underset{1-1\; onto}{⟶}N\setminus \left\{K\right\}\to Q:N\setminus \left\{K\right\}⟶N\setminus \left\{K\right\}$$
8		fdm	$$⊢Q:N\setminus \left\{K\right\}⟶N\setminus \left\{K\right\}\to \mathrm{dom}Q=N\setminus \left\{K\right\}$$
9		difssd	$$⊢\mathrm{dom}Q=N\setminus \left\{K\right\}\to Q\setminus \mathrm{I}\subseteq Q$$
10		dmss	$$⊢Q\setminus \mathrm{I}\subseteq Q\to \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\subseteq \mathrm{dom}Q$$
11	9 10	syl	$$⊢\mathrm{dom}Q=N\setminus \left\{K\right\}\to \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\subseteq \mathrm{dom}Q$$
12		difssd	$$⊢\mathrm{dom}Q=N\setminus \left\{K\right\}\to N\setminus \left\{K\right\}\subseteq N$$
13		sseq1	$$⊢\mathrm{dom}Q=N\setminus \left\{K\right\}\to \left(\mathrm{dom}Q\subseteq N\leftrightarrow N\setminus \left\{K\right\}\subseteq N\right)$$
14	12 13	mpbird	$$⊢\mathrm{dom}Q=N\setminus \left\{K\right\}\to \mathrm{dom}Q\subseteq N$$
15	11 14	sstrd	$$⊢\mathrm{dom}Q=N\setminus \left\{K\right\}\to \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\subseteq N$$
16	7 8 15	3syl	$$⊢Q:N\setminus \left\{K\right\}\underset{1-1\; onto}{⟶}N\setminus \left\{K\right\}\to \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\subseteq N$$
17		id	$$⊢\mathrm{dom}\left(Q\setminus \mathrm{I}\right)\approx 2_{𝑜}\to \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\approx 2_{𝑜}$$
18		eqid	$$⊢\mathrm{pmTrsp}\left(N\right)=\mathrm{pmTrsp}\left(N\right)$$
19	18 2	pmtrrn	$$⊢\left(N\in \mathrm{V}\wedge \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\subseteq N\wedge \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)\to \mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(Q\setminus \mathrm{I}\right)\right)\in R$$
20	3 19	eqeltrid	$$⊢\left(N\in \mathrm{V}\wedge \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\subseteq N\wedge \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)\to S\in R$$
21	6 16 17 20	syl3an	$$⊢\left(N\setminus \left\{K\right\}\in \mathrm{V}\wedge Q:N\setminus \left\{K\right\}\underset{1-1\; onto}{⟶}N\setminus \left\{K\right\}\wedge \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)\to S\in R$$
22	5 21	sylbi	$$⊢Q\in T\to S\in R$$