tocyccntz

Description: All elements of a (finite) set of cycles commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 27-Nov-2023)

	Ref	Expression
Hypotheses	tocyccntz.s	$⊢ S = SymGrp (D)$
	tocyccntz.z	$⊢ Z = Cntz (S)$
	tocyccntz.m	$⊢ M = toCyc (D)$
	tocyccntz.1	$⊢ φ \to D \in V$
	tocyccntz.2	$⊢ φ \to \underset{x \in A}{Disj} ran x$
	tocyccntz.a	$⊢ φ \to A \subseteq dom M$
Assertion	tocyccntz	$⊢ φ \to M [A] \subseteq Z (M [A])$

Proof

Step	Hyp	Ref	Expression
1		tocyccntz.s	$⊢ S = SymGrp (D)$
2		tocyccntz.z	$⊢ Z = Cntz (S)$
3		tocyccntz.m	$⊢ M = toCyc (D)$
4		tocyccntz.1	$⊢ φ \to D \in V$
5		tocyccntz.2	$⊢ φ \to \underset{x \in A}{Disj} ran x$
6		tocyccntz.a	$⊢ φ \to A \subseteq dom M$
7		eqid	$⊢ {Base}_{S} = {Base}_{S}$
8	3 1 7	tocycf	$⊢ D \in V \to M : \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
9		fimass	$⊢ M : \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\} ⟶ {Base}_{S} \to M [A] \subseteq {Base}_{S}$
10	4 8 9	3syl	$⊢ φ \to M [A] \subseteq {Base}_{S}$
11		difss	$⊢ A ∖ {\|.\|}^{-1} [\{0, 1\}] \subseteq A$
12		disjss1	$⊢ A ∖ {\|.\|}^{-1} [\{0, 1\}] \subseteq A \to (\underset{x \in A}{Disj} ran x \to \underset{x \in A ∖ {\|.\|}^{-1} [\{0, 1\}]}{Disj} ran x)$
13	11 5 12	mpsyl	$⊢ φ \to \underset{x \in A ∖ {\|.\|}^{-1} [\{0, 1\}]}{Disj} ran x$
14	4	adantr	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to D \in V$
15	6	adantr	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to A \subseteq dom M$
16		simpr	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])$
17	16	eldifad	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to x \in A$
18	15 17	sseldd	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to x \in dom M$
19		fdm	$⊢ M : \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\} ⟶ {Base}_{S} \to dom M = \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\}$
20	14 8 19	3syl	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to dom M = \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\}$
21	18 20	eleqtrd	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to x \in \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\}$
22		id	$⊢ c = x \to c = x$
23		dmeq	$⊢ c = x \to dom c = dom x$
24		eqidd	$⊢ c = x \to D = D$
25	22 23 24	f1eq123d	$⊢ c = x \to (c : dom c \underset{1-1}{⟶} D \leftrightarrow x : dom x \underset{1-1}{⟶} D)$
26	25	elrab	$⊢ x \in \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\} \leftrightarrow (x \in Word D \land x : dom x \underset{1-1}{⟶} D)$
27	21 26	sylib	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to (x \in Word D \land x : dom x \underset{1-1}{⟶} D)$
28	27	simpld	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to x \in Word D$
29	27	simprd	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to x : dom x \underset{1-1}{⟶} D$
30	16	eldifbd	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to \neg x \in {\|.\|}^{-1} [\{0, 1\}]$
31		hashgt1	$⊢ x \in V \to (\neg x \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow 1 < \|x\|)$
32	31	elv	$⊢ \neg x \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow 1 < \|x\|$
33	30 32	sylib	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to 1 < \|x\|$
34	3 14 28 29 33	cycpmrn	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to ran x = dom (M (x) ∖ I)$
35	16	fvresd	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) = M (x)$
36	35	difeq1d	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) ∖ I = M (x) ∖ I$
37	36	dmeqd	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to dom (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) ∖ I) = dom (M (x) ∖ I)$
38	34 37	eqtr4d	$⊢ (φ \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to ran x = dom (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) ∖ I)$
39	38	disjeq2dv	$⊢ φ \to (\underset{x \in A ∖ {\|.\|}^{-1} [\{0, 1\}]}{Disj} ran x \leftrightarrow \underset{x \in A ∖ {\|.\|}^{-1} [\{0, 1\}]}{Disj} dom (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) ∖ I))$
40	13 39	mpbid	$⊢ φ \to \underset{x \in A ∖ {\|.\|}^{-1} [\{0, 1\}]}{Disj} dom (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) ∖ I)$
41	4 8	syl	$⊢ φ \to M : \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
42	41	ffdmd	$⊢ φ \to M : dom M ⟶ {Base}_{S}$
43	6	ssdifssd	$⊢ φ \to A ∖ {\|.\|}^{-1} [\{0, 1\}] \subseteq dom M$
44	42 43	fssresd	$⊢ φ \to ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) : A ∖ {\|.\|}^{-1} [\{0, 1\}] ⟶ {Base}_{S}$
45	41 6	fssdmd	$⊢ φ \to A \subseteq \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\}$
46	45	ad4antr	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to A \subseteq \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\}$
47		simp-4r	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])$
48	47	eldifad	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to s \in A$
49	46 48	sseldd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to s \in \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\}$
50		id	$⊢ c = s \to c = s$
51		dmeq	$⊢ c = s \to dom c = dom s$
52		eqidd	$⊢ c = s \to D = D$
53	50 51 52	f1eq123d	$⊢ c = s \to (c : dom c \underset{1-1}{⟶} D \leftrightarrow s : dom s \underset{1-1}{⟶} D)$
54	53	elrab	$⊢ s \in \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\} \leftrightarrow (s \in Word D \land s : dom s \underset{1-1}{⟶} D)$
55	49 54	sylib	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to (s \in Word D \land s : dom s \underset{1-1}{⟶} D)$
56	55	simpld	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to s \in Word D$
57		wrdf	$⊢ s \in Word D \to s : (0 ..^\|s\|) ⟶ D$
58		frel	$⊢ s : (0 ..^\|s\|) ⟶ D \to Rel s$
59	56 57 58	3syl	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to Rel s$
60		simplr	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)$
61	47	fvresd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = M (s)$
62	16	ad5ant13	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])$
63	62	fvresd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) = M (x)$
64	60 61 63	3eqtr3rd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to M (x) = M (s)$
65	64	difeq1d	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to M (x) ∖ I = M (s) ∖ I$
66	65	dmeqd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to dom (M (x) ∖ I) = dom (M (s) ∖ I)$
67	4	ad4antr	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to D \in V$
68	17	ad5ant13	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to x \in A$
69	46 68	sseldd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to x \in \{c \in Word D \| c : dom c \underset{1-1}{⟶} D\}$
70	69 26	sylib	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to (x \in Word D \land x : dom x \underset{1-1}{⟶} D)$
71	70	simpld	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to x \in Word D$
72	70	simprd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to x : dom x \underset{1-1}{⟶} D$
73	33	ad5ant13	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to 1 < \|x\|$
74	3 67 71 72 73	cycpmrn	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ran x = dom (M (x) ∖ I)$
75	55	simprd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to s : dom s \underset{1-1}{⟶} D$
76	6	ssdifd	$⊢ φ \to A ∖ {\|.\|}^{-1} [\{0, 1\}] \subseteq dom M ∖ {\|.\|}^{-1} [\{0, 1\}]$
77	76	sselda	$⊢ (φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to s \in (dom M ∖ {\|.\|}^{-1} [\{0, 1\}])$
78	77	ad3antrrr	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to s \in (dom M ∖ {\|.\|}^{-1} [\{0, 1\}])$
79	78	eldifbd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to \neg s \in {\|.\|}^{-1} [\{0, 1\}]$
80		hashgt1	$⊢ s \in A \to (\neg s \in {\|.\|}^{-1} [\{0, 1\}] \leftrightarrow 1 < \|s\|)$
81	80	biimpa	$⊢ (s \in A \land \neg s \in {\|.\|}^{-1} [\{0, 1\}]) \to 1 < \|s\|$
82	48 79 81	syl2anc	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to 1 < \|s\|$
83	3 67 56 75 82	cycpmrn	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ran s = dom (M (s) ∖ I)$
84	66 74 83	3eqtr4rd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ran s = ran x$
85	84	ineq2d	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ran x \cap ran s = ran x \cap ran x$
86		inidm	$⊢ ran x \cap ran x = ran x$
87	85 86	eqtrdi	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ran x \cap ran s = ran x$
88		rneq	$⊢ x = y \to ran x = ran y$
89	88	cbvdisjv	$⊢ \underset{x \in A}{Disj} ran x \leftrightarrow \underset{y \in A}{Disj} ran y$
90	5 89	sylib	$⊢ φ \to \underset{y \in A}{Disj} ran y$
91	90	ad4antr	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to \underset{y \in A}{Disj} ran y$
92		simpr	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to \neg s = x$
93	92	neqned	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to s \neq x$
94	93	necomd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to x \neq s$
95		rneq	$⊢ y = x \to ran y = ran x$
96		rneq	$⊢ y = s \to ran y = ran s$
97	95 96	disji2	$⊢ (\underset{y \in A}{Disj} ran y \land (x \in A \land s \in A) \land x \neq s) \to ran x \cap ran s = \emptyset$
98	91 68 48 94 97	syl121anc	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ran x \cap ran s = \emptyset$
99	87 98	eqtr3d	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ran x = \emptyset$
100	84 99	eqtrd	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to ran s = \emptyset$
101		relrn0	$⊢ Rel s \to (s = \emptyset \leftrightarrow ran s = \emptyset)$
102	101	biimpar	$⊢ (Rel s \land ran s = \emptyset) \to s = \emptyset$
103	59 100 102	syl2anc	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to s = \emptyset$
104		wrdf	$⊢ x \in Word D \to x : (0 ..^\|x\|) ⟶ D$
105		frel	$⊢ x : (0 ..^\|x\|) ⟶ D \to Rel x$
106	71 104 105	3syl	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to Rel x$
107		relrn0	$⊢ Rel x \to (x = \emptyset \leftrightarrow ran x = \emptyset)$
108	107	biimpar	$⊢ (Rel x \land ran x = \emptyset) \to x = \emptyset$
109	106 99 108	syl2anc	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to x = \emptyset$
110	103 109	eqtr4d	$⊢ ((((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \land \neg s = x) \to s = x$
111	110	pm2.18da	$⊢ (((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \to s = x$
112	111	ex	$⊢ ((φ \land s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}])) \to (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) \to s = x)$
113	112	anasss	$⊢ (φ \land (s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}]) \land x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}]))) \to (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) \to s = x)$
114	113	ralrimivva	$⊢ φ \to \forall s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}]) \forall x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}]) (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) \to s = x)$
115		dff13	$⊢ ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) : A ∖ {\|.\|}^{-1} [\{0, 1\}] \underset{1-1}{⟶} {Base}_{S} \leftrightarrow (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) : A ∖ {\|.\|}^{-1} [\{0, 1\}] ⟶ {Base}_{S} \land \forall s \in (A ∖ {\|.\|}^{-1} [\{0, 1\}]) \forall x \in (A ∖ {\|.\|}^{-1} [\{0, 1\}]) (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (s) = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) \to s = x))$
116	44 114 115	sylanbrc	$⊢ φ \to ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) : A ∖ {\|.\|}^{-1} [\{0, 1\}] \underset{1-1}{⟶} {Base}_{S}$
117		f1f1orn	$⊢ ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) : A ∖ {\|.\|}^{-1} [\{0, 1\}] \underset{1-1}{⟶} {Base}_{S} \to ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) : A ∖ {\|.\|}^{-1} [\{0, 1\}] \underset{1-1 onto}{⟶} ran ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])})$
118	116 117	syl	$⊢ φ \to ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) : A ∖ {\|.\|}^{-1} [\{0, 1\}] \underset{1-1 onto}{⟶} ran ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])})$
119		df-ima	$⊢ M [A ∖ {\|.\|}^{-1} [\{0, 1\}]] = ran ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])})$
120	119	a1i	$⊢ φ \to M [A ∖ {\|.\|}^{-1} [\{0, 1\}]] = ran ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])})$
121	120	f1oeq3d	$⊢ φ \to (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) : A ∖ {\|.\|}^{-1} [\{0, 1\}] \underset{1-1 onto}{⟶} M [A ∖ {\|.\|}^{-1} [\{0, 1\}]] \leftrightarrow ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) : A ∖ {\|.\|}^{-1} [\{0, 1\}] \underset{1-1 onto}{⟶} ran ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}))$
122	118 121	mpbird	$⊢ φ \to ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) : A ∖ {\|.\|}^{-1} [\{0, 1\}] \underset{1-1 onto}{⟶} M [A ∖ {\|.\|}^{-1} [\{0, 1\}]]$
123		simpr	$⊢ (φ \land c = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \to c = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)$
124	123	difeq1d	$⊢ (φ \land c = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \to c ∖ I = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) ∖ I$
125	124	dmeqd	$⊢ (φ \land c = ({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x)) \to dom (c ∖ I) = dom (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) ∖ I)$
126	122 125	disjrdx	$⊢ φ \to (\underset{x \in A ∖ {\|.\|}^{-1} [\{0, 1\}]}{Disj} dom (({M ↾}_{(A ∖ {\|.\|}^{-1} [\{0, 1\}])}) (x) ∖ I) \leftrightarrow \underset{c \in M [A ∖ {\|.\|}^{-1} [\{0, 1\}]]}{Disj} dom (c ∖ I))$
127	40 126	mpbid	$⊢ φ \to \underset{c \in M [A ∖ {\|.\|}^{-1} [\{0, 1\}]]}{Disj} dom (c ∖ I)$
128		simpr	$⊢ (((φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \land x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])) \land M (x) = c) \to M (x) = c$
129	4	ad3antrrr	$⊢ (((φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \land x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])) \land M (x) = c) \to D \in V$
130	6	ssrind	$⊢ φ \to A \cap {\|.\|}^{-1} [\{0, 1\}] \subseteq dom M \cap {\|.\|}^{-1} [\{0, 1\}]$
131	130	ad3antrrr	$⊢ (((φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \land x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])) \land M (x) = c) \to A \cap {\|.\|}^{-1} [\{0, 1\}] \subseteq dom M \cap {\|.\|}^{-1} [\{0, 1\}]$
132		simplr	$⊢ (((φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \land x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])) \land M (x) = c) \to x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])$
133	131 132	sseldd	$⊢ (((φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \land x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])) \land M (x) = c) \to x \in (dom M \cap {\|.\|}^{-1} [\{0, 1\}])$
134	3	tocyc01	$⊢ (D \in V \land x \in (dom M \cap {\|.\|}^{-1} [\{0, 1\}])) \to M (x) = {I ↾}_{D}$
135	129 133 134	syl2anc	$⊢ (((φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \land x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])) \land M (x) = c) \to M (x) = {I ↾}_{D}$
136	128 135	eqtr3d	$⊢ (((φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \land x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])) \land M (x) = c) \to c = {I ↾}_{D}$
137	136	difeq1d	$⊢ (((φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \land x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])) \land M (x) = c) \to c ∖ I = ({I ↾}_{D}) ∖ I$
138	137	dmeqd	$⊢ (((φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \land x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])) \land M (x) = c) \to dom (c ∖ I) = dom (({I ↾}_{D}) ∖ I)$
139		resdifcom	$⊢ ({I ↾}_{D}) ∖ I = {(I ∖ I) ↾}_{D}$
140		difid	$⊢ I ∖ I = \emptyset$
141	140	reseq1i	$⊢ {(I ∖ I) ↾}_{D} = {\emptyset ↾}_{D}$
142		0res	$⊢ {\emptyset ↾}_{D} = \emptyset$
143	139 141 142	3eqtri	$⊢ ({I ↾}_{D}) ∖ I = \emptyset$
144	143	dmeqi	$⊢ dom (({I ↾}_{D}) ∖ I) = dom \emptyset$
145		dm0	$⊢ dom \emptyset = \emptyset$
146	144 145	eqtri	$⊢ dom (({I ↾}_{D}) ∖ I) = \emptyset$
147	138 146	eqtrdi	$⊢ (((φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \land x \in (A \cap {\|.\|}^{-1} [\{0, 1\}])) \land M (x) = c) \to dom (c ∖ I) = \emptyset$
148	41	ffund	$⊢ φ \to Fun M$
149		fvelima	$⊢ (Fun M \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \to \exists x \in (A \cap {\|.\|}^{-1} [\{0, 1\}]) M (x) = c$
150	148 149	sylan	$⊢ (φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \to \exists x \in (A \cap {\|.\|}^{-1} [\{0, 1\}]) M (x) = c$
151	147 150	r19.29a	$⊢ (φ \land c \in M [A \cap {\|.\|}^{-1} [\{0, 1\}]]) \to dom (c ∖ I) = \emptyset$
152	151	disjxun0	$⊢ φ \to (\underset{c \in M [A ∖ {\|.\|}^{-1} [\{0, 1\}]] \cup M [A \cap {\|.\|}^{-1} [\{0, 1\}]]}{Disj} dom (c ∖ I) \leftrightarrow \underset{c \in M [A ∖ {\|.\|}^{-1} [\{0, 1\}]]}{Disj} dom (c ∖ I))$
153	127 152	mpbird	$⊢ φ \to \underset{c \in M [A ∖ {\|.\|}^{-1} [\{0, 1\}]] \cup M [A \cap {\|.\|}^{-1} [\{0, 1\}]]}{Disj} dom (c ∖ I)$
154		uncom	$⊢ M [A ∖ {\|.\|}^{-1} [\{0, 1\}]] \cup M [A \cap {\|.\|}^{-1} [\{0, 1\}]] = M [A \cap {\|.\|}^{-1} [\{0, 1\}]] \cup M [A ∖ {\|.\|}^{-1} [\{0, 1\}]]$
155		imaundi	$⊢ M [(A \cap {\|.\|}^{-1} [\{0, 1\}]) \cup (A ∖ {\|.\|}^{-1} [\{0, 1\}])] = M [A \cap {\|.\|}^{-1} [\{0, 1\}]] \cup M [A ∖ {\|.\|}^{-1} [\{0, 1\}]]$
156		inundif	$⊢ (A \cap {\|.\|}^{-1} [\{0, 1\}]) \cup (A ∖ {\|.\|}^{-1} [\{0, 1\}]) = A$
157	156	imaeq2i	$⊢ M [(A \cap {\|.\|}^{-1} [\{0, 1\}]) \cup (A ∖ {\|.\|}^{-1} [\{0, 1\}])] = M [A]$
158	154 155 157	3eqtr2i	$⊢ M [A ∖ {\|.\|}^{-1} [\{0, 1\}]] \cup M [A \cap {\|.\|}^{-1} [\{0, 1\}]] = M [A]$
159	158	a1i	$⊢ φ \to M [A ∖ {\|.\|}^{-1} [\{0, 1\}]] \cup M [A \cap {\|.\|}^{-1} [\{0, 1\}]] = M [A]$
160	159	disjeq1d	$⊢ φ \to (\underset{c \in M [A ∖ {\|.\|}^{-1} [\{0, 1\}]] \cup M [A \cap {\|.\|}^{-1} [\{0, 1\}]]}{Disj} dom (c ∖ I) \leftrightarrow \underset{c \in M [A]}{Disj} dom (c ∖ I))$
161	153 160	mpbid	$⊢ φ \to \underset{c \in M [A]}{Disj} dom (c ∖ I)$
162	1 7 2 10 161	symgcntz	$⊢ φ \to M [A] \subseteq Z (M [A])$

Metamath Proof Explorer

Theorem tocyccntz

Proof