psgnfzto1stlem - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > psgnfzto1stlem		Structured version Visualization version Unicode version

Theorem psgnfzto1stlem 29850

Description: Lemma for psgnfzto1st 29855. Our permutation of rank

can be written as a permutation of rank

composed with a transposition. (Contributed by Thierry Arnoux, 21-Aug-2020.)

**Hypothesis**
Ref	Expression
psgnfzto1st.d

**Assertion**
Ref	Expression
psgnfzto1stlem	$/\$ pmTrsp

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem psgnfzto1stlem Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 6678	. . . . 5
2		ovex 6678	. . . . . 6
3		vex 3203	. . . . . 6
4	2, 3	ifex 4156	. . . . 5
5	1, 4	ifex 4156	. . . 4
6		eqid 2622	. . . 4
7	5, 6	fnmpti 6022	. . 3
8	7	a1i 11	. 2 $/\$
9		psgnfzto1st.d	. . . . 5
10		eqid 2622	. . . . 5 pmTrsp pmTrsp
11	9, 10	pmtrto1cl 29849	. . . 4 $/\$ pmTrsp pmTrsp
12		eqid 2622	. . . . 5 pmTrsp pmTrsp
13	10, 12	pmtrff1o 17883	. . . 4 pmTrsp pmTrsp pmTrsp
14		f1ofn 6138	. . . 4 pmTrsp pmTrsp
15	11, 13, 14	3syl 18	. . 3 $/\$ pmTrsp
16		simpr 477	. . . . . . . 8 $/\$ $/\$ $/\$
17	16	iftrued 4094	. . . . . . 7 $/\$ $/\$ $/\$
18		simpl 473	. . . . . . . . . 10 $/\$
19	18	nnred 11035	. . . . . . . . . . 11 $/\$
20		fz1ssnn 12372	. . . . . . . . . . . . 13
21	9	eleq2i 2693	. . . . . . . . . . . . . . 15
22	21	biimpi 206	. . . . . . . . . . . . . 14
23	22	adantl 482	. . . . . . . . . . . . 13 $/\$
24	20, 23	sseldi 3601	. . . . . . . . . . . 12 $/\$
25	24	nnred 11035	. . . . . . . . . . 11 $/\$
26		elfz1b 12409	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	26	simp2bi 1077	. . . . . . . . . . . . . 14
28	22, 27	syl 17	. . . . . . . . . . . . 13
29	28	adantl 482	. . . . . . . . . . . 12 $/\$
30	29	nnred 11035	. . . . . . . . . . 11 $/\$
31	19	lep1d 10955	. . . . . . . . . . 11 $/\$
32		elfzle2 12345	. . . . . . . . . . . 12
33	23, 32	syl 17	. . . . . . . . . . 11 $/\$
34	19, 25, 30, 31, 33	letrd 10194	. . . . . . . . . 10 $/\$
35	29	nnzd 11481	. . . . . . . . . . 11 $/\$
36		fznn 12408	. . . . . . . . . . 11 $/\$
37	35, 36	syl 17	. . . . . . . . . 10 $/\$ $/\$
38	18, 34, 37	mpbir2and 957	. . . . . . . . 9 $/\$
39	38, 9	syl6eleqr 2712	. . . . . . . 8 $/\$
40	39	ad2antrr 762	. . . . . . 7 $/\$ $/\$ $/\$
41	17, 40	eqeltrd 2701	. . . . . 6 $/\$ $/\$ $/\$
42		simpr 477	. . . . . . . 8 $/\$ $/\$ $/\$
43	42	iffalsed 4097	. . . . . . 7 $/\$ $/\$ $/\$
44		simpr 477	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
45	44	iftrued 4094	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
46	42	adantr 481	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
47	9, 20	eqsstri 3635	. . . . . . . . . . . . . . . 16
48		simpllr 799	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
49	47, 48	sseldi 3601	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
50		nn1m1nn 11040	. . . . . . . . . . . . . . 15 $\/$
51	49, 50	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\/$
52	51	ord 392	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
53	46, 52	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
54	53	nnred 11035	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
55	49	nnred 11035	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
56	30	ad3antrrr 766	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
57	55	lem1d 10957	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
58	48, 9	syl6eleq 2711	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
59		elfzle2 12345	. . . . . . . . . . . . . 14
60	58, 59	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
61	54, 55, 56, 57, 60	letrd 10194	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
62	53, 61	jca 554	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
63		fznn 12408	. . . . . . . . . . . . 13 $/\$
64	35, 63	syl 17	. . . . . . . . . . . 12 $/\$ $/\$
65	64	ad3antrrr 766	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
66	62, 65	mpbird 247	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
67	66, 9	syl6eleqr 2712	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
68	45, 67	eqeltrd 2701	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
69		simpr 477	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
70	69	iffalsed 4097	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
71		simpllr 799	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
72	70, 71	eqeltrd 2701	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
73	68, 72	pm2.61dan 832	. . . . . . 7 $/\$ $/\$ $/\$
74	43, 73	eqeltrd 2701	. . . . . 6 $/\$ $/\$ $/\$
75	41, 74	pm2.61dan 832	. . . . 5 $/\$ $/\$
76	75	ralrimiva 2966	. . . 4 $/\$
77		eqid 2622	. . . . 5
78	77	fnmpt 6020	. . . 4
79	76, 78	syl 17	. . 3 $/\$
80	77	rnmptss 6392	. . . 4
81	76, 80	syl 17	. . 3 $/\$
82		fnco 5999	. . 3 pmTrsp $/\$ $/\$ pmTrsp
83	15, 79, 81, 82	syl3anc 1326	. 2 $/\$ pmTrsp
84		simpr 477	. . . . . . . 8 $/\$ $/\$ $/\$
85	84	iftrued 4094	. . . . . . 7 $/\$ $/\$ $/\$
86	85	fveq2d 6195	. . . . . 6 $/\$ $/\$ $/\$ pmTrsp pmTrsp
87		fzfi 12771	. . . . . . . . . 10
88	9, 87	eqeltri 2697	. . . . . . . . 9
89	88	a1i 11	. . . . . . . 8 $/\$
90	23, 21	sylibr 224	. . . . . . . 8 $/\$
91	19	ltp1d 10954	. . . . . . . . 9 $/\$
92	19, 91	ltned 10173	. . . . . . . 8 $/\$
93	10	pmtrprfv 17873	. . . . . . . 8 $/\$ $/\$ $/\$ pmTrsp
94	89, 39, 90, 92, 93	syl13anc 1328	. . . . . . 7 $/\$ pmTrsp
95	94	ad2antrr 762	. . . . . 6 $/\$ $/\$ $/\$ pmTrsp
96	86, 95	eqtr2d 2657	. . . . 5 $/\$ $/\$ $/\$ pmTrsp
97	88	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
98	39	ad4antr 768	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
99	90	ad4antr 768	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
100	92	ad4antr 768	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
101	10	pmtrprfv2 29848	. . . . . . . . . 10 $/\$ $/\$ $/\$ pmTrsp
102	97, 98, 99, 100, 101	syl13anc 1328	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ pmTrsp
103	91	ad4antr 768	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
104		simpr 477	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
105	103, 104	breqtrrd 4681	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
106	19	ad4antr 768	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
107		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
108	47, 107	sseldi 3601	. . . . . . . . . . . . . . . 16 $/\$ $/\$
109	108	nnred 11035	. . . . . . . . . . . . . . 15 $/\$ $/\$
110	109	ad3antrrr 766	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
111	106, 110	ltnled 10184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
112	105, 111	mpbid 222	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
113	112	iffalsed 4097	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
114	113, 104	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
115	114	fveq2d 6195	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ pmTrsp pmTrsp
116	104	oveq1d 6665	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
117	106	recnd 10068	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
118		1cnd 10056	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
119	117, 118	pncand 10393	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
120	116, 119	eqtrd 2656	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
121	102, 115, 120	3eqtr4rd 2667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ pmTrsp
122		simplr 792	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
123		simpr 477	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
124	123	necomd 2849	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
125	109	ad3antrrr 766	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
126	25	ad4antr 768	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
127	125, 126	ltlend 10182	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128	122, 124, 127	mpbir2and 957	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
129	108	ad3antrrr 766	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
130		simpll 790	. . . . . . . . . . . . . 14 $/\$ $/\$
131	130	ad3antrrr 766	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
132		nnleltp1 11432	. . . . . . . . . . . . 13 $/\$
133	129, 131, 132	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
134	128, 133	mpbird 247	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
135	134	iftrued 4094	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
136	135	fveq2d 6195	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ pmTrsp pmTrsp
137	88	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
138	39	ad4antr 768	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
139		simp-5r 809	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
140		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
141	140	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
142		elnn1uz2 11765	. . . . . . . . . . . . . . . . . 18 $\/$
143	129, 142	sylib 208	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
144	143	ord 392	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
145	141, 144	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
146		uz2m1nn 11763	. . . . . . . . . . . . . . 15
147	145, 146	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
148	139, 28	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
149	147	nnred 11035	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
150	131, 139, 30	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
151	125	lem1d 10957	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
152	107	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
153	152, 9	syl6eleq 2711	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
154		elfzle2 12345	. . . . . . . . . . . . . . . 16
155	153, 154	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
156	149, 125, 150, 151, 155	letrd 10194	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
157	147, 148, 156	3jca 1242	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158		elfz1b 12409	. . . . . . . . . . . . 13 $/\$ $/\$
159	157, 158	sylibr 224	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
160	159, 9	syl6eleqr 2712	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
161	138, 139, 160	3jca 1242	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	131, 139, 92	syl2anc 693	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
163		simpr 477	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
164	163	oveq1d 6665	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
165	109	recnd 10068	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	165	ad3antrrr 766	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
167		1cnd 10056	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
168	166, 167	npcand 10396	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
169	164, 168	eqtr2d 2657	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
170	169	ex 450	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
171	170	necon3d 2815	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
172	171	imp 445	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
173	149, 125, 126, 151, 128	lelttrd 10195	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
174	149, 173	ltned 10173	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
175	174	necomd 2849	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
176	162, 172, 175	3jca 1242	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	10	pmtrprfv3 17874	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ pmTrsp
178	137, 161, 176, 177	syl3anc 1326	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ pmTrsp
179	136, 178	eqtr2d 2657	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ pmTrsp
180	121, 179	pm2.61dane 2881	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ pmTrsp
181	109	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
182	19	ad3antrrr 766	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
183	25	ad3antrrr 766	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
184		simpr 477	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
185	31	ad3antrrr 766	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
186	181, 182, 183, 184, 185	letrd 10194	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
187	186	ex 450	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
188	187	con3d 148	. . . . . . . . . . 11 $/\$ $/\$ $/\$
189	188	imp 445	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
190	189	iffalsed 4097	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
191	190	fveq2d 6195	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ pmTrsp pmTrsp
192	88	a1i 11	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
193	39	ad3antrrr 766	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
194	90	ad3antrrr 766	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
195	107	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
196	193, 194, 195	3jca 1242	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
197	92	ad3antrrr 766	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
198	19	ad3antrrr 766	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
199	25	ad3antrrr 766	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
200	109	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
201	91	ad3antrrr 766	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
202		simpr 477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
203	199, 200	ltnled 10184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
204	202, 203	mpbird 247	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
205	198, 199, 200, 201, 204	lttrd 10198	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
206	198, 205	ltned 10173	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
207	199, 204	ltned 10173	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
208	197, 206, 207	3jca 1242	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
209	10	pmtrprfv3 17874	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ pmTrsp
210	192, 196, 208, 209	syl3anc 1326	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ pmTrsp
211	191, 210	eqtr2d 2657	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ pmTrsp
212	180, 211	ifeqda 4121	. . . . . 6 $/\$ $/\$ $/\$ pmTrsp
213	140	iffalsed 4097	. . . . . . 7 $/\$ $/\$ $/\$
214	213	fveq2d 6195	. . . . . 6 $/\$ $/\$ $/\$ pmTrsp pmTrsp
215	212, 214	eqtr4d 2659	. . . . 5 $/\$ $/\$ $/\$ pmTrsp
216	96, 215	ifeqda 4121	. . . 4 $/\$ $/\$ pmTrsp
217		eqidd 2623	. . . . . 6 $/\$ $/\$
218		eqeq1 2626	. . . . . . . 8
219		breq1 4656	. . . . . . . . 9
220		oveq1 6657	. . . . . . . . 9
221		id 22	. . . . . . . . 9
222	219, 220, 221	ifbieq12d 4113	. . . . . . . 8
223	218, 222	ifbieq2d 4111	. . . . . . 7
224	223	adantl 482	. . . . . 6 $/\$ $/\$ $/\$
225		ovex 6678	. . . . . . . . 9
226		vex 3203	. . . . . . . . 9
227	225, 226	keepel 4155	. . . . . . . 8
228	227	a1i 11	. . . . . . 7 $/\$ $/\$
229		ifexg 4157	. . . . . . 7 $/\$
230	130, 228, 229	syl2anc 693	. . . . . 6 $/\$ $/\$
231	217, 224, 107, 230	fvmptd 6288	. . . . 5 $/\$ $/\$
232	231	fveq2d 6195	. . . 4 $/\$ $/\$ pmTrsp pmTrsp
233	216, 232	eqtr4d 2659	. . 3 $/\$ $/\$ pmTrsp
234		breq1 4656	. . . . . . 7
235	234, 220, 221	ifbieq12d 4113	. . . . . 6
236	218, 235	ifbieq2d 4111	. . . . 5
237	225, 226	ifex 4156	. . . . . 6
238	1, 237	ifex 4156	. . . . 5
239	236, 6, 238	fvmpt 6282	. . . 4
240	239	adantl 482	. . 3 $/\$ $/\$
241		funmpt 5926	. . . . 5
242	241	a1i 11	. . . 4 $/\$ $/\$
243	76	adantr 481	. . . . . 6 $/\$ $/\$
244		dmmptg 5632	. . . . . 6
245	243, 244	syl 17	. . . . 5 $/\$ $/\$
246	107, 245	eleqtrrd 2704	. . . 4 $/\$ $/\$
247		fvco 6274	. . . 4 $/\$ pmTrsp pmTrsp
248	242, 246, 247	syl2anc 693	. . 3 $/\$ $/\$ pmTrsp pmTrsp
249	233, 240, 248	3eqtr4d 2666	. 2 $/\$ $/\$ pmTrsp
250	8, 83, 249	eqfnfvd 6314	1 $/\$ pmTrsp

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wral 2912

cvv 3200

wss 3574

cif 4086

cpr 4179 class class class wbr 4653

cmpt 4729

cdm 5114

crn 5115

ccom 5118

wfun 5882

wfn 5883

wf1o 5887

cfv 5888 (class class class)co 6650

cfn 7955

cc 9934

cr 9935

c1 9937

caddc 9939

clt 10074

cle 10075

cmin 10266

cn 11020

c2 11070

cz 11377

cuz 11687

cfz 12326 pmTrspcpmtr 17861

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-pmtr 17862

This theorem is referenced by: fzto1st 29853 psgnfzto1st 29855

W3C validator