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

Metamath Proof Explorer

Theorem symggen

Proof