pmtrdifellem4

	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	pmtrdifellem4	$⊢ (Q \in T \land K \in N) \to S (K) = K$

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	1 2 3	pmtrdifellem1	$⊢ Q \in T \to S \in R$
5		eqid	$⊢ pmTrsp (N) = pmTrsp (N)$
6		eqid	$⊢ dom (S ∖ I) = dom (S ∖ I)$
7	5 2 6	pmtrffv	$⊢ (S \in R \land K \in N) \to S (K) = if (K \in dom (S ∖ I), ⋃ (dom (S ∖ I) ∖ \{K\}), K)$
8	4 7	sylan	$⊢ (Q \in T \land K \in N) \to S (K) = if (K \in dom (S ∖ I), ⋃ (dom (S ∖ I) ∖ \{K\}), K)$
9		eqid	$⊢ SymGrp (N ∖ \{K\}) = SymGrp (N ∖ \{K\})$
10		eqid	$⊢ {Base}_{SymGrp (N ∖ \{K\})} = {Base}_{SymGrp (N ∖ \{K\})}$
11	1 9 10	symgtrf	$⊢ T \subseteq {Base}_{SymGrp (N ∖ \{K\})}$
12	11	sseli	$⊢ Q \in T \to Q \in {Base}_{SymGrp (N ∖ \{K\})}$
13	9 10	symgbasf	$⊢ Q \in {Base}_{SymGrp (N ∖ \{K\})} \to Q : N ∖ \{K\} ⟶ N ∖ \{K\}$
14		ffn	$⊢ Q : N ∖ \{K\} ⟶ N ∖ \{K\} \to Q Fn (N ∖ \{K\})$
15		fndifnfp	$⊢ Q Fn (N ∖ \{K\}) \to dom (Q ∖ I) = \{x \in (N ∖ \{K\}) \| Q (x) \neq x\}$
16		ssrab2	$⊢ \{x \in (N ∖ \{K\}) \| Q (x) \neq x\} \subseteq N ∖ \{K\}$
17		ssel2	$⊢ (\{x \in (N ∖ \{K\}) \| Q (x) \neq x\} \subseteq N ∖ \{K\} \land K \in \{x \in (N ∖ \{K\}) \| Q (x) \neq x\}) \to K \in (N ∖ \{K\})$
18		eldif	$⊢ K \in (N ∖ \{K\}) \leftrightarrow (K \in N \land \neg K \in \{K\})$
19		elsng	$⊢ K \in N \to (K \in \{K\} \leftrightarrow K = K)$
20	19	notbid	$⊢ K \in N \to (\neg K \in \{K\} \leftrightarrow \neg K = K)$
21		eqid	$⊢ K = K$
22	21	pm2.24i	$⊢ \neg K = K \to \neg K \in N$
23	20 22	syl6bi	$⊢ K \in N \to (\neg K \in \{K\} \to \neg K \in N)$
24	23	imp	$⊢ (K \in N \land \neg K \in \{K\}) \to \neg K \in N$
25	18 24	sylbi	$⊢ K \in (N ∖ \{K\}) \to \neg K \in N$
26	17 25	syl	$⊢ (\{x \in (N ∖ \{K\}) \| Q (x) \neq x\} \subseteq N ∖ \{K\} \land K \in \{x \in (N ∖ \{K\}) \| Q (x) \neq x\}) \to \neg K \in N$
27	16 26	mpan	$⊢ K \in \{x \in (N ∖ \{K\}) \| Q (x) \neq x\} \to \neg K \in N$
28	27	con2i	$⊢ K \in N \to \neg K \in \{x \in (N ∖ \{K\}) \| Q (x) \neq x\}$
29		eleq2	$⊢ dom (Q ∖ I) = \{x \in (N ∖ \{K\}) \| Q (x) \neq x\} \to (K \in dom (Q ∖ I) \leftrightarrow K \in \{x \in (N ∖ \{K\}) \| Q (x) \neq x\})$
30	29	notbid	$⊢ dom (Q ∖ I) = \{x \in (N ∖ \{K\}) \| Q (x) \neq x\} \to (\neg K \in dom (Q ∖ I) \leftrightarrow \neg K \in \{x \in (N ∖ \{K\}) \| Q (x) \neq x\})$
31	28 30	imbitrrid	$⊢ dom (Q ∖ I) = \{x \in (N ∖ \{K\}) \| Q (x) \neq x\} \to (K \in N \to \neg K \in dom (Q ∖ I))$
32	14 15 31	3syl	$⊢ Q : N ∖ \{K\} ⟶ N ∖ \{K\} \to (K \in N \to \neg K \in dom (Q ∖ I))$
33	12 13 32	3syl	$⊢ Q \in T \to (K \in N \to \neg K \in dom (Q ∖ I))$
34	33	imp	$⊢ (Q \in T \land K \in N) \to \neg K \in dom (Q ∖ I)$
35	1 2 3	pmtrdifellem2	$⊢ Q \in T \to dom (S ∖ I) = dom (Q ∖ I)$
36	35	eleq2d	$⊢ Q \in T \to (K \in dom (S ∖ I) \leftrightarrow K \in dom (Q ∖ I))$
37	36	adantr	$⊢ (Q \in T \land K \in N) \to (K \in dom (S ∖ I) \leftrightarrow K \in dom (Q ∖ I))$
38	34 37	mtbird	$⊢ (Q \in T \land K \in N) \to \neg K \in dom (S ∖ I)$
39	38	iffalsed	$⊢ (Q \in T \land K \in N) \to if (K \in dom (S ∖ I), ⋃ (dom (S ∖ I) ∖ \{K\}), K) = K$
40	8 39	eqtrd	$⊢ (Q \in T \land K \in N) \to S (K) = K$

Metamath Proof Explorer

Theorem pmtrdifellem4

Proof