symggen

Description: The span of the transpositions is the subgroup that moves finitely many points. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Hypotheses	symgtrf.t	$⊢ T = ran pmTrsp (D)$
	symgtrf.g	$⊢ G = SymGrp (D)$
	symgtrf.b	$⊢ B = {Base}_{G}$
	symggen.k	$⊢ K = mrCls (SubMnd (G))$
Assertion	symggen	$⊢ D \in V \to K (T) = \{x \in B \| dom (x ∖ I) \in Fin\}$

Proof

Step	Hyp	Ref	Expression
1		symgtrf.t	$⊢ T = ran pmTrsp (D)$
2		symgtrf.g	$⊢ G = SymGrp (D)$
3		symgtrf.b	$⊢ B = {Base}_{G}$
4		symggen.k	$⊢ K = mrCls (SubMnd (G))$
5		elex	$⊢ D \in V \to D \in V$
6	2	symggrp	$⊢ D \in V \to G \in Grp$
7		grpmnd	$⊢ G \in Grp \to G \in Mnd$
8	6 7	syl	$⊢ D \in V \to G \in Mnd$
9	3	submacs	$⊢ G \in Mnd \to SubMnd (G) \in ACS (B)$
10		acsmre	$⊢ SubMnd (G) \in ACS (B) \to SubMnd (G) \in Moore (B)$
11	8 9 10	3syl	$⊢ D \in V \to SubMnd (G) \in Moore (B)$
12	5 11	syl	$⊢ D \in V \to SubMnd (G) \in Moore (B)$
13	1 2 3	symgtrf	$⊢ T \subseteq B$
14	13	a1i	$⊢ D \in V \to T \subseteq B$
15		2onn	$⊢ 2_{𝑜} \in ω$
16		nnfi	$⊢ 2_{𝑜} \in ω \to 2_{𝑜} \in Fin$
17	15 16	ax-mp	$⊢ 2_{𝑜} \in Fin$
18		eqid	$⊢ pmTrsp (D) = pmTrsp (D)$
19	18 1	pmtrfb	$⊢ x \in T \leftrightarrow (D \in V \land x : D \underset{1-1 onto}{⟶} D \land dom (x ∖ I) \approx 2_{𝑜})$
20	19	simp3bi	$⊢ x \in T \to dom (x ∖ I) \approx 2_{𝑜}$
21		enfi	$⊢ dom (x ∖ I) \approx 2_{𝑜} \to (dom (x ∖ I) \in Fin \leftrightarrow 2_{𝑜} \in Fin)$
22	20 21	syl	$⊢ x \in T \to (dom (x ∖ I) \in Fin \leftrightarrow 2_{𝑜} \in Fin)$
23	22	adantl	$⊢ (D \in V \land x \in T) \to (dom (x ∖ I) \in Fin \leftrightarrow 2_{𝑜} \in Fin)$
24	17 23	mpbiri	$⊢ (D \in V \land x \in T) \to dom (x ∖ I) \in Fin$
25	14 24	ssrabdv	$⊢ D \in V \to T \subseteq \{x \in B \| dom (x ∖ I) \in Fin\}$
26	2 3	symgfisg	$⊢ D \in V \to \{x \in B \| dom (x ∖ I) \in Fin\} \in SubGrp (G)$
27		subgsubm	$⊢ \{x \in B \| dom (x ∖ I) \in Fin\} \in SubGrp (G) \to \{x \in B \| dom (x ∖ I) \in Fin\} \in SubMnd (G)$
28	26 27	syl	$⊢ D \in V \to \{x \in B \| dom (x ∖ I) \in Fin\} \in SubMnd (G)$
29	4	mrcsscl	$⊢ (SubMnd (G) \in Moore (B) \land T \subseteq \{x \in B \| dom (x ∖ I) \in Fin\} \land \{x \in B \| dom (x ∖ I) \in Fin\} \in SubMnd (G)) \to K (T) \subseteq \{x \in B \| dom (x ∖ I) \in Fin\}$
30	12 25 28 29	syl3anc	$⊢ D \in V \to K (T) \subseteq \{x \in B \| dom (x ∖ I) \in Fin\}$
31		vex	$⊢ x \in V$
32	31	a1i	$⊢ dom (x ∖ I) \in Fin \to x \in V$
33		finnum	$⊢ dom (x ∖ I) \in Fin \to dom (x ∖ I) \in dom card$
34		domfi	$⊢ (dom (x ∖ I) \in Fin \land dom (y ∖ I) ≼ dom (x ∖ I)) \to dom (y ∖ I) \in Fin$
35	2 3	symgbasf1o	$⊢ y \in B \to y : D \underset{1-1 onto}{⟶} D$
36	35	adantl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to y : D \underset{1-1 onto}{⟶} D$
37		f1ofn	$⊢ y : D \underset{1-1 onto}{⟶} D \to y Fn D$
38		fnnfpeq0	$⊢ y Fn D \to (dom (y ∖ I) = \emptyset \leftrightarrow y = {I ↾}_{D})$
39	36 37 38	3syl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to (dom (y ∖ I) = \emptyset \leftrightarrow y = {I ↾}_{D})$
40	2 3	elbasfv	$⊢ y \in B \to D \in V$
41	40	adantl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to D \in V$
42	2	symgid	$⊢ D \in V \to {I ↾}_{D} = 0_{G}$
43	41 42	syl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to {I ↾}_{D} = 0_{G}$
44	41 11	syl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to SubMnd (G) \in Moore (B)$
45	4	mrccl	$⊢ (SubMnd (G) \in Moore (B) \land T \subseteq B) \to K (T) \in SubMnd (G)$
46	44 13 45	sylancl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to K (T) \in SubMnd (G)$
47		eqid	$⊢ 0_{G} = 0_{G}$
48	47	subm0cl	$⊢ K (T) \in SubMnd (G) \to 0_{G} \in K (T)$
49	46 48	syl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to 0_{G} \in K (T)$
50	43 49	eqeltrd	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to {I ↾}_{D} \in K (T)$
51		eleq1a	$⊢ {I ↾}_{D} \in K (T) \to (y = {I ↾}_{D} \to y \in K (T))$
52	50 51	syl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to (y = {I ↾}_{D} \to y \in K (T))$
53	39 52	sylbid	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to (dom (y ∖ I) = \emptyset \to y \in K (T))$
54	53	adantr	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \to (dom (y ∖ I) = \emptyset \to y \in K (T))$
55		n0	$⊢ dom (y ∖ I) \neq \emptyset \leftrightarrow \exists u u \in dom (y ∖ I)$
56	41	adantr	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to D \in V$
57		simpr	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to u \in dom (y ∖ I)$
58		f1omvdmvd	$⊢ (y : D \underset{1-1 onto}{⟶} D \land u \in dom (y ∖ I)) \to y (u) \in (dom (y ∖ I) ∖ \{u\})$
59	36 58	sylan	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to y (u) \in (dom (y ∖ I) ∖ \{u\})$
60	59	eldifad	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to y (u) \in dom (y ∖ I)$
61	57 60	prssd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to \{u, y (u)\} \subseteq dom (y ∖ I)$
62		difss	$⊢ y ∖ I \subseteq y$
63		dmss	$⊢ y ∖ I \subseteq y \to dom (y ∖ I) \subseteq dom y$
64	62 63	ax-mp	$⊢ dom (y ∖ I) \subseteq dom y$
65		f1odm	$⊢ y : D \underset{1-1 onto}{⟶} D \to dom y = D$
66	36 65	syl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to dom y = D$
67	64 66	sseqtrid	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to dom (y ∖ I) \subseteq D$
68	67	adantr	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom (y ∖ I) \subseteq D$
69	61 68	sstrd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to \{u, y (u)\} \subseteq D$
70		vex	$⊢ u \in V$
71		fvex	$⊢ y (u) \in V$
72	36	adantr	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to y : D \underset{1-1 onto}{⟶} D$
73	72 37	syl	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to y Fn D$
74	67	sselda	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to u \in D$
75		fnelnfp	$⊢ (y Fn D \land u \in D) \to (u \in dom (y ∖ I) \leftrightarrow y (u) \neq u)$
76	73 74 75	syl2anc	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to (u \in dom (y ∖ I) \leftrightarrow y (u) \neq u)$
77	57 76	mpbid	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to y (u) \neq u$
78	77	necomd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to u \neq y (u)$
79		pr2nelem	$⊢ (u \in V \land y (u) \in V \land u \neq y (u)) \to \{u, y (u)\} \approx 2_{𝑜}$
80	70 71 78 79	mp3an12i	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to \{u, y (u)\} \approx 2_{𝑜}$
81	18 1	pmtrrn	$⊢ (D \in V \land \{u, y (u)\} \subseteq D \land \{u, y (u)\} \approx 2_{𝑜}) \to pmTrsp (D) (\{u, y (u)\}) \in T$
82	56 69 80 81	syl3anc	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) \in T$
83	13 82	sseldi	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) \in B$
84		simplr	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to y \in B$
85		eqid	$⊢ +_{G} = +_{G}$
86	2 3 85	symgov	$⊢ (pmTrsp (D) (\{u, y (u)\}) \in B \land y \in B) \to pmTrsp (D) (\{u, y (u)\}) +_{G} y = pmTrsp (D) (\{u, y (u)\}) \circ y$
87	83 84 86	syl2anc	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) +_{G} y = pmTrsp (D) (\{u, y (u)\}) \circ y$
88	87	oveq2d	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) +_{G} (pmTrsp (D) (\{u, y (u)\}) +_{G} y) = pmTrsp (D) (\{u, y (u)\}) +_{G} (pmTrsp (D) (\{u, y (u)\}) \circ y)$
89	41 6	syl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to G \in Grp$
90	89	adantr	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to G \in Grp$
91	3 85	grpcl	$⊢ (G \in Grp \land pmTrsp (D) (\{u, y (u)\}) \in B \land y \in B) \to pmTrsp (D) (\{u, y (u)\}) +_{G} y \in B$
92	90 83 84 91	syl3anc	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) +_{G} y \in B$
93	87 92	eqeltrrd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) \circ y \in B$
94	2 3 85	symgov	$⊢ (pmTrsp (D) (\{u, y (u)\}) \in B \land pmTrsp (D) (\{u, y (u)\}) \circ y \in B) \to pmTrsp (D) (\{u, y (u)\}) +_{G} (pmTrsp (D) (\{u, y (u)\}) \circ y) = pmTrsp (D) (\{u, y (u)\}) \circ (pmTrsp (D) (\{u, y (u)\}) \circ y)$
95	83 93 94	syl2anc	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) +_{G} (pmTrsp (D) (\{u, y (u)\}) \circ y) = pmTrsp (D) (\{u, y (u)\}) \circ (pmTrsp (D) (\{u, y (u)\}) \circ y)$
96		coass	$⊢ (pmTrsp (D) (\{u, y (u)\}) \circ pmTrsp (D) (\{u, y (u)\})) \circ y = pmTrsp (D) (\{u, y (u)\}) \circ (pmTrsp (D) (\{u, y (u)\}) \circ y)$
97	18 1	pmtrfinv	$⊢ pmTrsp (D) (\{u, y (u)\}) \in T \to pmTrsp (D) (\{u, y (u)\}) \circ pmTrsp (D) (\{u, y (u)\}) = {I ↾}_{D}$
98	82 97	syl	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) \circ pmTrsp (D) (\{u, y (u)\}) = {I ↾}_{D}$
99	98	coeq1d	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to (pmTrsp (D) (\{u, y (u)\}) \circ pmTrsp (D) (\{u, y (u)\})) \circ y = ({I ↾}_{D}) \circ y$
100		f1of	$⊢ y : D \underset{1-1 onto}{⟶} D \to y : D ⟶ D$
101		fcoi2	$⊢ y : D ⟶ D \to ({I ↾}_{D}) \circ y = y$
102	72 100 101	3syl	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to ({I ↾}_{D}) \circ y = y$
103	99 102	eqtrd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to (pmTrsp (D) (\{u, y (u)\}) \circ pmTrsp (D) (\{u, y (u)\})) \circ y = y$
104	96 103	syl5eqr	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) \circ (pmTrsp (D) (\{u, y (u)\}) \circ y) = y$
105	88 95 104	3eqtrd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) +_{G} (pmTrsp (D) (\{u, y (u)\}) +_{G} y) = y$
106	105	adantlr	$⊢ (((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) +_{G} (pmTrsp (D) (\{u, y (u)\}) +_{G} y) = y$
107	46	ad2antrr	$⊢ (((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \land u \in dom (y ∖ I)) \to K (T) \in SubMnd (G)$
108	4	mrcssid	$⊢ (SubMnd (G) \in Moore (B) \land T \subseteq B) \to T \subseteq K (T)$
109	44 13 108	sylancl	$⊢ (dom (y ∖ I) \in Fin \land y \in B) \to T \subseteq K (T)$
110	109	adantr	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to T \subseteq K (T)$
111	110 82	sseldd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) \in K (T)$
112	111	adantlr	$⊢ (((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) \in K (T)$
113	87	difeq1d	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to (pmTrsp (D) (\{u, y (u)\}) +_{G} y) ∖ I = (pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I$
114	113	dmeqd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom ((pmTrsp (D) (\{u, y (u)\}) +_{G} y) ∖ I) = dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I)$
115		simpll	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom (y ∖ I) \in Fin$
116		mvdco	$⊢ dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I) \subseteq dom (pmTrsp (D) (\{u, y (u)\}) ∖ I) \cup dom (y ∖ I)$
117	18	pmtrmvd	$⊢ (D \in V \land \{u, y (u)\} \subseteq D \land \{u, y (u)\} \approx 2_{𝑜}) \to dom (pmTrsp (D) (\{u, y (u)\}) ∖ I) = \{u, y (u)\}$
118	56 69 80 117	syl3anc	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom (pmTrsp (D) (\{u, y (u)\}) ∖ I) = \{u, y (u)\}$
119	118 61	eqsstrd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom (pmTrsp (D) (\{u, y (u)\}) ∖ I) \subseteq dom (y ∖ I)$
120		ssidd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom (y ∖ I) \subseteq dom (y ∖ I)$
121	119 120	unssd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom (pmTrsp (D) (\{u, y (u)\}) ∖ I) \cup dom (y ∖ I) \subseteq dom (y ∖ I)$
122	116 121	sstrid	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I) \subseteq dom (y ∖ I)$
123		fvco2	$⊢ (y Fn D \land u \in D) \to (pmTrsp (D) (\{u, y (u)\}) \circ y) (u) = pmTrsp (D) (\{u, y (u)\}) (y (u))$
124	73 74 123	syl2anc	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to (pmTrsp (D) (\{u, y (u)\}) \circ y) (u) = pmTrsp (D) (\{u, y (u)\}) (y (u))$
125		prcom	$⊢ \{u, y (u)\} = \{y (u), u\}$
126	125	fveq2i	$⊢ pmTrsp (D) (\{u, y (u)\}) = pmTrsp (D) (\{y (u), u\})$
127	126	fveq1i	$⊢ pmTrsp (D) (\{u, y (u)\}) (y (u)) = pmTrsp (D) (\{y (u), u\}) (y (u))$
128	68 60	sseldd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to y (u) \in D$
129	18	pmtrprfv	$⊢ (D \in V \land (y (u) \in D \land u \in D \land y (u) \neq u)) \to pmTrsp (D) (\{y (u), u\}) (y (u)) = u$
130	56 128 74 77 129	syl13anc	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{y (u), u\}) (y (u)) = u$
131	127 130	syl5eq	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) (y (u)) = u$
132	124 131	eqtrd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to (pmTrsp (D) (\{u, y (u)\}) \circ y) (u) = u$
133	2 3	symgbasf1o	$⊢ pmTrsp (D) (\{u, y (u)\}) \circ y \in B \to (pmTrsp (D) (\{u, y (u)\}) \circ y) : D \underset{1-1 onto}{⟶} D$
134		f1ofn	$⊢ (pmTrsp (D) (\{u, y (u)\}) \circ y) : D \underset{1-1 onto}{⟶} D \to (pmTrsp (D) (\{u, y (u)\}) \circ y) Fn D$
135	93 133 134	3syl	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to (pmTrsp (D) (\{u, y (u)\}) \circ y) Fn D$
136		fnelnfp	$⊢ ((pmTrsp (D) (\{u, y (u)\}) \circ y) Fn D \land u \in D) \to (u \in dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I) \leftrightarrow (pmTrsp (D) (\{u, y (u)\}) \circ y) (u) \neq u)$
137	136	necon2bbid	$⊢ ((pmTrsp (D) (\{u, y (u)\}) \circ y) Fn D \land u \in D) \to ((pmTrsp (D) (\{u, y (u)\}) \circ y) (u) = u \leftrightarrow \neg u \in dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I))$
138	135 74 137	syl2anc	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to ((pmTrsp (D) (\{u, y (u)\}) \circ y) (u) = u \leftrightarrow \neg u \in dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I))$
139	132 138	mpbid	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to \neg u \in dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I)$
140	122 57 139	ssnelpssd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I) \subset dom (y ∖ I)$
141		php3	$⊢ (dom (y ∖ I) \in Fin \land dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I) \subset dom (y ∖ I)) \to dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I) ≺ dom (y ∖ I)$
142	115 140 141	syl2anc	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom ((pmTrsp (D) (\{u, y (u)\}) \circ y) ∖ I) ≺ dom (y ∖ I)$
143	114 142	eqbrtrd	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land u \in dom (y ∖ I)) \to dom ((pmTrsp (D) (\{u, y (u)\}) +_{G} y) ∖ I) ≺ dom (y ∖ I)$
144	143	adantlr	$⊢ (((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \land u \in dom (y ∖ I)) \to dom ((pmTrsp (D) (\{u, y (u)\}) +_{G} y) ∖ I) ≺ dom (y ∖ I)$
145	92	adantlr	$⊢ (((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) +_{G} y \in B$
146		ovex	$⊢ pmTrsp (D) (\{u, y (u)\}) +_{G} y \in V$
147		difeq1	$⊢ z = pmTrsp (D) (\{u, y (u)\}) +_{G} y \to z ∖ I = (pmTrsp (D) (\{u, y (u)\}) +_{G} y) ∖ I$
148	147	dmeqd	$⊢ z = pmTrsp (D) (\{u, y (u)\}) +_{G} y \to dom (z ∖ I) = dom ((pmTrsp (D) (\{u, y (u)\}) +_{G} y) ∖ I)$
149	148	breq1d	$⊢ z = pmTrsp (D) (\{u, y (u)\}) +_{G} y \to (dom (z ∖ I) ≺ dom (y ∖ I) \leftrightarrow dom ((pmTrsp (D) (\{u, y (u)\}) +_{G} y) ∖ I) ≺ dom (y ∖ I))$
150		eleq1	$⊢ z = pmTrsp (D) (\{u, y (u)\}) +_{G} y \to (z \in B \leftrightarrow pmTrsp (D) (\{u, y (u)\}) +_{G} y \in B)$
151		eleq1	$⊢ z = pmTrsp (D) (\{u, y (u)\}) +_{G} y \to (z \in K (T) \leftrightarrow pmTrsp (D) (\{u, y (u)\}) +_{G} y \in K (T))$
152	150 151	imbi12d	$⊢ z = pmTrsp (D) (\{u, y (u)\}) +_{G} y \to ((z \in B \to z \in K (T)) \leftrightarrow (pmTrsp (D) (\{u, y (u)\}) +_{G} y \in B \to pmTrsp (D) (\{u, y (u)\}) +_{G} y \in K (T)))$
153	149 152	imbi12d	$⊢ z = pmTrsp (D) (\{u, y (u)\}) +_{G} y \to ((dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T))) \leftrightarrow (dom ((pmTrsp (D) (\{u, y (u)\}) +_{G} y) ∖ I) ≺ dom (y ∖ I) \to (pmTrsp (D) (\{u, y (u)\}) +_{G} y \in B \to pmTrsp (D) (\{u, y (u)\}) +_{G} y \in K (T))))$
154	146 153	spcv	$⊢ \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T))) \to (dom ((pmTrsp (D) (\{u, y (u)\}) +_{G} y) ∖ I) ≺ dom (y ∖ I) \to (pmTrsp (D) (\{u, y (u)\}) +_{G} y \in B \to pmTrsp (D) (\{u, y (u)\}) +_{G} y \in K (T)))$
155	154	ad2antlr	$⊢ (((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \land u \in dom (y ∖ I)) \to (dom ((pmTrsp (D) (\{u, y (u)\}) +_{G} y) ∖ I) ≺ dom (y ∖ I) \to (pmTrsp (D) (\{u, y (u)\}) +_{G} y \in B \to pmTrsp (D) (\{u, y (u)\}) +_{G} y \in K (T)))$
156	144 145 155	mp2d	$⊢ (((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) +_{G} y \in K (T)$
157	85	submcl	$⊢ (K (T) \in SubMnd (G) \land pmTrsp (D) (\{u, y (u)\}) \in K (T) \land pmTrsp (D) (\{u, y (u)\}) +_{G} y \in K (T)) \to pmTrsp (D) (\{u, y (u)\}) +_{G} (pmTrsp (D) (\{u, y (u)\}) +_{G} y) \in K (T)$
158	107 112 156 157	syl3anc	$⊢ (((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \land u \in dom (y ∖ I)) \to pmTrsp (D) (\{u, y (u)\}) +_{G} (pmTrsp (D) (\{u, y (u)\}) +_{G} y) \in K (T)$
159	106 158	eqeltrrd	$⊢ (((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \land u \in dom (y ∖ I)) \to y \in K (T)$
160	159	ex	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \to (u \in dom (y ∖ I) \to y \in K (T))$
161	160	exlimdv	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \to (\exists u u \in dom (y ∖ I) \to y \in K (T))$
162	55 161	syl5bi	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \to (dom (y ∖ I) \neq \emptyset \to y \in K (T))$
163	54 162	pm2.61dne	$⊢ ((dom (y ∖ I) \in Fin \land y \in B) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \to y \in K (T)$
164	163	exp31	$⊢ dom (y ∖ I) \in Fin \to (y \in B \to (\forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T))) \to y \in K (T)))$
165	164	com23	$⊢ dom (y ∖ I) \in Fin \to (\forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T))) \to (y \in B \to y \in K (T)))$
166	34 165	syl	$⊢ (dom (x ∖ I) \in Fin \land dom (y ∖ I) ≼ dom (x ∖ I)) \to (\forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T))) \to (y \in B \to y \in K (T)))$
167	166	3impia	$⊢ (dom (x ∖ I) \in Fin \land dom (y ∖ I) ≼ dom (x ∖ I) \land \forall z (dom (z ∖ I) ≺ dom (y ∖ I) \to (z \in B \to z \in K (T)))) \to (y \in B \to y \in K (T))$
168		eleq1w	$⊢ y = z \to (y \in B \leftrightarrow z \in B)$
169		eleq1w	$⊢ y = z \to (y \in K (T) \leftrightarrow z \in K (T))$
170	168 169	imbi12d	$⊢ y = z \to ((y \in B \to y \in K (T)) \leftrightarrow (z \in B \to z \in K (T)))$
171		eleq1w	$⊢ y = x \to (y \in B \leftrightarrow x \in B)$
172		eleq1w	$⊢ y = x \to (y \in K (T) \leftrightarrow x \in K (T))$
173	171 172	imbi12d	$⊢ y = x \to ((y \in B \to y \in K (T)) \leftrightarrow (x \in B \to x \in K (T)))$
174		difeq1	$⊢ y = z \to y ∖ I = z ∖ I$
175	174	dmeqd	$⊢ y = z \to dom (y ∖ I) = dom (z ∖ I)$
176		difeq1	$⊢ y = x \to y ∖ I = x ∖ I$
177	176	dmeqd	$⊢ y = x \to dom (y ∖ I) = dom (x ∖ I)$
178	32 33 167 170 173 175 177	indcardi	$⊢ dom (x ∖ I) \in Fin \to (x \in B \to x \in K (T))$
179	178	impcom	$⊢ (x \in B \land dom (x ∖ I) \in Fin) \to x \in K (T)$
180	179	3adant1	$⊢ (D \in V \land x \in B \land dom (x ∖ I) \in Fin) \to x \in K (T)$
181	180	rabssdv	$⊢ D \in V \to \{x \in B \| dom (x ∖ I) \in Fin\} \subseteq K (T)$
182	30 181	eqssd	$⊢ D \in V \to K (T) = \{x \in B \| dom (x ∖ I) \in Fin\}$

Metamath Proof Explorer

Theorem symggen

Proof