symgfix2

Description: If a permutation does not move a certain element of a set to a second element, there is a third element which is moved to the second element. (Contributed by AV, 2-Jan-2019)

		Ref	Expression
	Hypothesis	symgfix2.p	$⊢ P = {Base}_{SymGrp (N)}$
	Assertion	symgfix2	$⊢ L \in N \to (Q \in (P ∖ \{q \in P \| q (K) = L\}) \to \exists k \in (N ∖ \{K\}) Q (k) = L)$

Proof

Step	Hyp	Ref	Expression
1		symgfix2.p	$⊢ P = {Base}_{SymGrp (N)}$
2		eldif	$⊢ Q \in (P ∖ \{q \in P \| q (K) = L\}) \leftrightarrow (Q \in P \land \neg Q \in \{q \in P \| q (K) = L\})$
3		ianor	$⊢ \neg (Q \in P \land Q (K) = L) \leftrightarrow (\neg Q \in P \lor \neg Q (K) = L)$
4		fveq1	$⊢ q = Q \to q (K) = Q (K)$
5	4	eqeq1d	$⊢ q = Q \to (q (K) = L \leftrightarrow Q (K) = L)$
6	5	elrab	$⊢ Q \in \{q \in P \| q (K) = L\} \leftrightarrow (Q \in P \land Q (K) = L)$
7	3 6	xchnxbir	$⊢ \neg Q \in \{q \in P \| q (K) = L\} \leftrightarrow (\neg Q \in P \lor \neg Q (K) = L)$
8	7	anbi2i	$⊢ (Q \in P \land \neg Q \in \{q \in P \| q (K) = L\}) \leftrightarrow (Q \in P \land (\neg Q \in P \lor \neg Q (K) = L))$
9	2 8	bitri	$⊢ Q \in (P ∖ \{q \in P \| q (K) = L\}) \leftrightarrow (Q \in P \land (\neg Q \in P \lor \neg Q (K) = L))$
10		pm2.21	$⊢ \neg Q \in P \to (Q \in P \to (L \in N \to \exists k \in (N ∖ \{K\}) Q (k) = L))$
11	1	symgmov2	$⊢ Q \in P \to \forall l \in N \exists k \in N Q (k) = l$
12		eqeq2	$⊢ l = L \to (Q (k) = l \leftrightarrow Q (k) = L)$
13	12	rexbidv	$⊢ l = L \to (\exists k \in N Q (k) = l \leftrightarrow \exists k \in N Q (k) = L)$
14	13	rspcva	$⊢ (L \in N \land \forall l \in N \exists k \in N Q (k) = l) \to \exists k \in N Q (k) = L$
15		eqeq2	$⊢ L = Q (k) \to (Q (K) = L \leftrightarrow Q (K) = Q (k))$
16	15	eqcoms	$⊢ Q (k) = L \to (Q (K) = L \leftrightarrow Q (K) = Q (k))$
17	16	notbid	$⊢ Q (k) = L \to (\neg Q (K) = L \leftrightarrow \neg Q (K) = Q (k))$
18		fveq2	$⊢ K = k \to Q (K) = Q (k)$
19	18	eqcoms	$⊢ k = K \to Q (K) = Q (k)$
20	19	necon3bi	$⊢ \neg Q (K) = Q (k) \to k \neq K$
21	17 20	syl6bi	$⊢ Q (k) = L \to (\neg Q (K) = L \to k \neq K)$
22	21	com12	$⊢ \neg Q (K) = L \to (Q (k) = L \to k \neq K)$
23	22	pm4.71rd	$⊢ \neg Q (K) = L \to (Q (k) = L \leftrightarrow (k \neq K \land Q (k) = L))$
24	23	rexbidv	$⊢ \neg Q (K) = L \to (\exists k \in N Q (k) = L \leftrightarrow \exists k \in N (k \neq K \land Q (k) = L))$
25		rexdifsn	$⊢ \exists k \in (N ∖ \{K\}) Q (k) = L \leftrightarrow \exists k \in N (k \neq K \land Q (k) = L)$
26	24 25	bitr4di	$⊢ \neg Q (K) = L \to (\exists k \in N Q (k) = L \leftrightarrow \exists k \in (N ∖ \{K\}) Q (k) = L)$
27	14 26	syl5ibcom	$⊢ (L \in N \land \forall l \in N \exists k \in N Q (k) = l) \to (\neg Q (K) = L \to \exists k \in (N ∖ \{K\}) Q (k) = L)$
28	27	ex	$⊢ L \in N \to (\forall l \in N \exists k \in N Q (k) = l \to (\neg Q (K) = L \to \exists k \in (N ∖ \{K\}) Q (k) = L))$
29	28	com13	$⊢ \neg Q (K) = L \to (\forall l \in N \exists k \in N Q (k) = l \to (L \in N \to \exists k \in (N ∖ \{K\}) Q (k) = L))$
30	11 29	syl5	$⊢ \neg Q (K) = L \to (Q \in P \to (L \in N \to \exists k \in (N ∖ \{K\}) Q (k) = L))$
31	10 30	jaoi	$⊢ (\neg Q \in P \lor \neg Q (K) = L) \to (Q \in P \to (L \in N \to \exists k \in (N ∖ \{K\}) Q (k) = L))$
32	31	com13	$⊢ L \in N \to (Q \in P \to ((\neg Q \in P \lor \neg Q (K) = L) \to \exists k \in (N ∖ \{K\}) Q (k) = L))$
33	32	impd	$⊢ L \in N \to ((Q \in P \land (\neg Q \in P \lor \neg Q (K) = L)) \to \exists k \in (N ∖ \{K\}) Q (k) = L)$
34	9 33	biimtrid	$⊢ L \in N \to (Q \in (P ∖ \{q \in P \| q (K) = L\}) \to \exists k \in (N ∖ \{K\}) Q (k) = L)$

Metamath Proof Explorer

Theorem symgfix2

Proof