pmtrdifellem1

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

Proof

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

Metamath Proof Explorer

Theorem pmtrdifellem1

Proof