pmtrdifellem2

	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	pmtrdifellem2	$⊢ Q \in T \to dom (S ∖ I) = dom (Q ∖ I)$

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	3	difeq1i	$⊢ S ∖ I = pmTrsp (N) (dom (Q ∖ I)) ∖ I$
5	4	dmeqi	$⊢ dom (S ∖ I) = dom (pmTrsp (N) (dom (Q ∖ I)) ∖ I)$
6		eqid	$⊢ pmTrsp (N ∖ \{K\}) = pmTrsp (N ∖ \{K\})$
7	6 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_{𝑜})$
8		difsnexi	$⊢ N ∖ \{K\} \in V \to N \in V$
9		f1of	$⊢ Q : N ∖ \{K\} \underset{1-1 onto}{⟶} N ∖ \{K\} \to Q : N ∖ \{K\} ⟶ N ∖ \{K\}$
10		fdm	$⊢ Q : N ∖ \{K\} ⟶ N ∖ \{K\} \to dom Q = N ∖ \{K\}$
11		difssd	$⊢ dom Q = N ∖ \{K\} \to Q ∖ I \subseteq Q$
12		dmss	$⊢ Q ∖ I \subseteq Q \to dom (Q ∖ I) \subseteq dom Q$
13	11 12	syl	$⊢ dom Q = N ∖ \{K\} \to dom (Q ∖ I) \subseteq dom Q$
14		difssd	$⊢ dom Q = N ∖ \{K\} \to N ∖ \{K\} \subseteq N$
15		sseq1	$⊢ dom Q = N ∖ \{K\} \to (dom Q \subseteq N \leftrightarrow N ∖ \{K\} \subseteq N)$
16	14 15	mpbird	$⊢ dom Q = N ∖ \{K\} \to dom Q \subseteq N$
17	13 16	sstrd	$⊢ dom Q = N ∖ \{K\} \to dom (Q ∖ I) \subseteq N$
18	9 10 17	3syl	$⊢ Q : N ∖ \{K\} \underset{1-1 onto}{⟶} N ∖ \{K\} \to dom (Q ∖ I) \subseteq N$
19		id	$⊢ dom (Q ∖ I) \approx 2_{𝑜} \to dom (Q ∖ I) \approx 2_{𝑜}$
20	8 18 19	3anim123i	$⊢ (N ∖ \{K\} \in V \land Q : N ∖ \{K\} \underset{1-1 onto}{⟶} N ∖ \{K\} \land dom (Q ∖ I) \approx 2_{𝑜}) \to (N \in V \land dom (Q ∖ I) \subseteq N \land dom (Q ∖ I) \approx 2_{𝑜})$
21	7 20	sylbi	$⊢ Q \in T \to (N \in V \land dom (Q ∖ I) \subseteq N \land dom (Q ∖ I) \approx 2_{𝑜})$
22		eqid	$⊢ pmTrsp (N) = pmTrsp (N)$
23	22	pmtrmvd	$⊢ (N \in V \land dom (Q ∖ I) \subseteq N \land dom (Q ∖ I) \approx 2_{𝑜}) \to dom (pmTrsp (N) (dom (Q ∖ I)) ∖ I) = dom (Q ∖ I)$
24	21 23	syl	$⊢ Q \in T \to dom (pmTrsp (N) (dom (Q ∖ I)) ∖ I) = dom (Q ∖ I)$
25	5 24	eqtrid	$⊢ Q \in T \to dom (S ∖ I) = dom (Q ∖ I)$

Metamath Proof Explorer

Theorem pmtrdifellem2

Proof