Theorem 1idprl 7147

Description: Lemma for 1idpr 7149. (Contributed by Jim Kingdon, 13-Dec-2019.)

Assertion

Ref	Expression
1idprl	|- ( A e. P. -> ( 1st ` ( A .P. 1P ) ) = ( 1st ` A ) )

Proof of Theorem 1idprl

Dummy variables x y z w v u f g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 3044	. . . . . 6 |- ( 1st ` 1P ) C_ ( 1st ` 1P )
2		rexss 3088	. . . . . 6 |- ( ( 1st ` 1P ) C_ ( 1st ` 1P ) -> ( E. g e. ( 1st ` 1P ) x = ( f .Q g ) <-> E. g e. ( 1st ` 1P ) ( g e. ( 1st ` 1P ) /\ x = ( f .Q g ) ) ) )
3	1, 2	ax-mp 7	. . . . 5 |- ( E. g e. ( 1st ` 1P ) x = ( f .Q g ) <-> E. g e. ( 1st ` 1P ) ( g e. ( 1st ` 1P ) /\ x = ( f .Q g ) ) )
4		r19.42v 2524	. . . . . 6 |- ( E. g e. ( 1st ` 1P ) ( x <Q f /\ x = ( f .Q g ) ) <-> ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) )
5		1pr 7111	. . . . . . . . . . 11 |- 1P e. P.
6		prop 7032	. . . . . . . . . . . 12 |- ( 1P e. P. -> <. ( 1st ` 1P ) , ( 2nd ` 1P ) >. e. P. )
7		elprnql 7038	. . . . . . . . . . . 12 |- ( ( <. ( 1st ` 1P ) , ( 2nd ` 1P ) >. e. P. /\ g e. ( 1st ` 1P ) ) -> g e. Q. )
8	6, 7	sylan 277	. . . . . . . . . . 11 |- ( ( 1P e. P. /\ g e. ( 1st ` 1P ) ) -> g e. Q. )
9	5, 8	mpan 415	. . . . . . . . . 10 |- ( g e. ( 1st ` 1P ) -> g e. Q. )
10		prop 7032	. . . . . . . . . . . 12 |- ( A e. P. -> <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. )
11		elprnql 7038	. . . . . . . . . . . 12 |- ( ( <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. /\ f e. ( 1st ` A ) ) -> f e. Q. )
12	10, 11	sylan 277	. . . . . . . . . . 11 |- ( ( A e. P. /\ f e. ( 1st ` A ) ) -> f e. Q. )
13		breq1 3848	. . . . . . . . . . . . 13 |- ( x = ( f .Q g ) -> ( x <Q f <-> ( f .Q g ) <Q f ) )
14	13	3ad2ant3 966	. . . . . . . . . . . 12 |- ( ( f e. Q. /\ g e. Q. /\ x = ( f .Q g ) ) -> ( x <Q f <-> ( f .Q g ) <Q f ) )
15		1prl 7112	. . . . . . . . . . . . . . 15 |- ( 1st ` 1P ) = { g | g <Q 1Q }
16	15	abeq2i 2198	. . . . . . . . . . . . . 14 |- ( g e. ( 1st ` 1P ) <-> g <Q 1Q )
17		1nq 6923	. . . . . . . . . . . . . . . . 17 |- 1Q e. Q.
18		ltmnqg 6958	. . . . . . . . . . . . . . . . 17 |- ( ( g e. Q. /\ 1Q e. Q. /\ f e. Q. ) -> ( g <Q 1Q <-> ( f .Q g ) <Q ( f .Q 1Q ) ) )
19	17, 18	mp3an2 1261	. . . . . . . . . . . . . . . 16 |- ( ( g e. Q. /\ f e. Q. ) -> ( g <Q 1Q <-> ( f .Q g ) <Q ( f .Q 1Q ) ) )
20	19	ancoms 264	. . . . . . . . . . . . . . 15 |- ( ( f e. Q. /\ g e. Q. ) -> ( g <Q 1Q <-> ( f .Q g ) <Q ( f .Q 1Q ) ) )
21		mulidnq 6946	. . . . . . . . . . . . . . . . 17 |- ( f e. Q. -> ( f .Q 1Q ) = f )
22	21	breq2d 3857	. . . . . . . . . . . . . . . 16 |- ( f e. Q. -> ( ( f .Q g ) <Q ( f .Q 1Q ) <-> ( f .Q g ) <Q f ) )
23	22	adantr 270	. . . . . . . . . . . . . . 15 |- ( ( f e. Q. /\ g e. Q. ) -> ( ( f .Q g ) <Q ( f .Q 1Q ) <-> ( f .Q g ) <Q f ) )
24	20, 23	bitrd 186	. . . . . . . . . . . . . 14 |- ( ( f e. Q. /\ g e. Q. ) -> ( g <Q 1Q <-> ( f .Q g ) <Q f ) )
25	16, 24	syl5rbb 191	. . . . . . . . . . . . 13 |- ( ( f e. Q. /\ g e. Q. ) -> ( ( f .Q g ) <Q f <-> g e. ( 1st ` 1P ) ) )
26	25	3adant3 963	. . . . . . . . . . . 12 |- ( ( f e. Q. /\ g e. Q. /\ x = ( f .Q g ) ) -> ( ( f .Q g ) <Q f <-> g e. ( 1st ` 1P ) ) )
27	14, 26	bitrd 186	. . . . . . . . . . 11 |- ( ( f e. Q. /\ g e. Q. /\ x = ( f .Q g ) ) -> ( x <Q f <-> g e. ( 1st ` 1P ) ) )
28	12, 27	syl3an1 1207	. . . . . . . . . 10 |- ( ( ( A e. P. /\ f e. ( 1st ` A ) ) /\ g e. Q. /\ x = ( f .Q g ) ) -> ( x <Q f <-> g e. ( 1st ` 1P ) ) )
29	9, 28	syl3an2 1208	. . . . . . . . 9 |- ( ( ( A e. P. /\ f e. ( 1st ` A ) ) /\ g e. ( 1st ` 1P ) /\ x = ( f .Q g ) ) -> ( x <Q f <-> g e. ( 1st ` 1P ) ) )
30	29	3expia 1145	. . . . . . . 8 |- ( ( ( A e. P. /\ f e. ( 1st ` A ) ) /\ g e. ( 1st ` 1P ) ) -> ( x = ( f .Q g ) -> ( x <Q f <-> g e. ( 1st ` 1P ) ) ) )
31	30	pm5.32rd 439	. . . . . . 7 |- ( ( ( A e. P. /\ f e. ( 1st ` A ) ) /\ g e. ( 1st ` 1P ) ) -> ( ( x <Q f /\ x = ( f .Q g ) ) <-> ( g e. ( 1st ` 1P ) /\ x = ( f .Q g ) ) ) )
32	31	rexbidva 2377	. . . . . 6 |- ( ( A e. P. /\ f e. ( 1st ` A ) ) -> ( E. g e. ( 1st ` 1P ) ( x <Q f /\ x = ( f .Q g ) ) <-> E. g e. ( 1st ` 1P ) ( g e. ( 1st ` 1P ) /\ x = ( f .Q g ) ) ) )
33	4, 32	syl5rbbr 193	. . . . 5 |- ( ( A e. P. /\ f e. ( 1st ` A ) ) -> ( E. g e. ( 1st ` 1P ) ( g e. ( 1st ` 1P ) /\ x = ( f .Q g ) ) <-> ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) ) )
34	3, 33	syl5bb 190	. . . 4 |- ( ( A e. P. /\ f e. ( 1st ` A ) ) -> ( E. g e. ( 1st ` 1P ) x = ( f .Q g ) <-> ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) ) )
35	34	rexbidva 2377	. . 3 |- ( A e. P. -> ( E. f e. ( 1st ` A ) E. g e. ( 1st ` 1P ) x = ( f .Q g ) <-> E. f e. ( 1st ` A ) ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) ) )
36		df-imp 7026	. . . . 5 |- .P. = ( y e. P. , z e. P. |-> <. { w e. Q. | E. u e. Q. E. v e. Q. ( u e. ( 1st ` y ) /\ v e. ( 1st ` z ) /\ w = ( u .Q v ) ) } , { w e. Q. | E. u e. Q. E. v e. Q. ( u e. ( 2nd ` y ) /\ v e. ( 2nd ` z ) /\ w = ( u .Q v ) ) } >. )
37		mulclnq 6933	. . . . 5 |- ( ( u e. Q. /\ v e. Q. ) -> ( u .Q v ) e. Q. )
38	36, 37	genpelvl 7069	. . . 4 |- ( ( A e. P. /\ 1P e. P. ) -> ( x e. ( 1st ` ( A .P. 1P ) ) <-> E. f e. ( 1st ` A ) E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) )
39	5, 38	mpan2 416	. . 3 |- ( A e. P. -> ( x e. ( 1st ` ( A .P. 1P ) ) <-> E. f e. ( 1st ` A ) E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) )
40		prnmaxl 7045	. . . . . . 7 |- ( ( <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. /\ x e. ( 1st ` A ) ) -> E. f e. ( 1st ` A ) x <Q f )
41	10, 40	sylan 277	. . . . . 6 |- ( ( A e. P. /\ x e. ( 1st ` A ) ) -> E. f e. ( 1st ` A ) x <Q f )
42		ltrelnq 6922	. . . . . . . . . . . . 13 |- <Q C_ ( Q. X. Q. )
43	42	brel 4490	. . . . . . . . . . . 12 |- ( x <Q f -> ( x e. Q. /\ f e. Q. ) )
44		ltmnqg 6958	. . . . . . . . . . . . . . . 16 |- ( ( y e. Q. /\ z e. Q. /\ w e. Q. ) -> ( y <Q z <-> ( w .Q y ) <Q ( w .Q z ) ) )
45	44	adantl 271	. . . . . . . . . . . . . . 15 |- ( ( ( x e. Q. /\ f e. Q. ) /\ ( y e. Q. /\ z e. Q. /\ w e. Q. ) ) -> ( y <Q z <-> ( w .Q y ) <Q ( w .Q z ) ) )
46		simpl 107	. . . . . . . . . . . . . . 15 |- ( ( x e. Q. /\ f e. Q. ) -> x e. Q. )
47		simpr 108	. . . . . . . . . . . . . . 15 |- ( ( x e. Q. /\ f e. Q. ) -> f e. Q. )
48		recclnq 6949	. . . . . . . . . . . . . . . 16 |- ( f e. Q. -> ( *Q ` f ) e. Q. )
49	48	adantl 271	. . . . . . . . . . . . . . 15 |- ( ( x e. Q. /\ f e. Q. ) -> ( *Q ` f ) e. Q. )
50		mulcomnqg 6940	. . . . . . . . . . . . . . . 16 |- ( ( y e. Q. /\ z e. Q. ) -> ( y .Q z ) = ( z .Q y ) )
51	50	adantl 271	. . . . . . . . . . . . . . 15 |- ( ( ( x e. Q. /\ f e. Q. ) /\ ( y e. Q. /\ z e. Q. ) ) -> ( y .Q z ) = ( z .Q y ) )
52	45, 46, 47, 49, 51	caovord2d 5814	. . . . . . . . . . . . . 14 |- ( ( x e. Q. /\ f e. Q. ) -> ( x <Q f <-> ( x .Q ( *Q ` f ) ) <Q ( f .Q ( *Q ` f ) ) ) )
53		recidnq 6950	. . . . . . . . . . . . . . . 16 |- ( f e. Q. -> ( f .Q ( *Q ` f ) ) = 1Q )
54	53	breq2d 3857	. . . . . . . . . . . . . . 15 |- ( f e. Q. -> ( ( x .Q ( *Q ` f ) ) <Q ( f .Q ( *Q ` f ) ) <-> ( x .Q ( *Q ` f ) ) <Q 1Q ) )
55	54	adantl 271	. . . . . . . . . . . . . 14 |- ( ( x e. Q. /\ f e. Q. ) -> ( ( x .Q ( *Q ` f ) ) <Q ( f .Q ( *Q ` f ) ) <-> ( x .Q ( *Q ` f ) ) <Q 1Q ) )
56	52, 55	bitrd 186	. . . . . . . . . . . . 13 |- ( ( x e. Q. /\ f e. Q. ) -> ( x <Q f <-> ( x .Q ( *Q ` f ) ) <Q 1Q ) )
57	56	biimpd 142	. . . . . . . . . . . 12 |- ( ( x e. Q. /\ f e. Q. ) -> ( x <Q f -> ( x .Q ( *Q ` f ) ) <Q 1Q ) )
58	43, 57	mpcom 36	. . . . . . . . . . 11 |- ( x <Q f -> ( x .Q ( *Q ` f ) ) <Q 1Q )
59		mulclnq 6933	. . . . . . . . . . . . . 14 |- ( ( x e. Q. /\ ( *Q ` f ) e. Q. ) -> ( x .Q ( *Q ` f ) ) e. Q. )
60	48, 59	sylan2 280	. . . . . . . . . . . . 13 |- ( ( x e. Q. /\ f e. Q. ) -> ( x .Q ( *Q ` f ) ) e. Q. )
61	43, 60	syl 14	. . . . . . . . . . . 12 |- ( x <Q f -> ( x .Q ( *Q ` f ) ) e. Q. )
62		breq1 3848	. . . . . . . . . . . . 13 |- ( g = ( x .Q ( *Q ` f ) ) -> ( g <Q 1Q <-> ( x .Q ( *Q ` f ) ) <Q 1Q ) )
63	62, 15	elab2g 2762	. . . . . . . . . . . 12 |- ( ( x .Q ( *Q ` f ) ) e. Q. -> ( ( x .Q ( *Q ` f ) ) e. ( 1st ` 1P ) <-> ( x .Q ( *Q ` f ) ) <Q 1Q ) )
64	61, 63	syl 14	. . . . . . . . . . 11 |- ( x <Q f -> ( ( x .Q ( *Q ` f ) ) e. ( 1st ` 1P ) <-> ( x .Q ( *Q ` f ) ) <Q 1Q ) )
65	58, 64	mpbird 165	. . . . . . . . . 10 |- ( x <Q f -> ( x .Q ( *Q ` f ) ) e. ( 1st ` 1P ) )
66		mulassnqg 6941	. . . . . . . . . . . . . 14 |- ( ( y e. Q. /\ z e. Q. /\ w e. Q. ) -> ( ( y .Q z ) .Q w ) = ( y .Q ( z .Q w ) ) )
67	66	adantl 271	. . . . . . . . . . . . 13 |- ( ( ( x e. Q. /\ f e. Q. ) /\ ( y e. Q. /\ z e. Q. /\ w e. Q. ) ) -> ( ( y .Q z ) .Q w ) = ( y .Q ( z .Q w ) ) )
68	47, 46, 49, 51, 67	caov12d 5826	. . . . . . . . . . . 12 |- ( ( x e. Q. /\ f e. Q. ) -> ( f .Q ( x .Q ( *Q ` f ) ) ) = ( x .Q ( f .Q ( *Q ` f ) ) ) )
69	53	oveq2d 5668	. . . . . . . . . . . . 13 |- ( f e. Q. -> ( x .Q ( f .Q ( *Q ` f ) ) ) = ( x .Q 1Q ) )
70	69	adantl 271	. . . . . . . . . . . 12 |- ( ( x e. Q. /\ f e. Q. ) -> ( x .Q ( f .Q ( *Q ` f ) ) ) = ( x .Q 1Q ) )
71		mulidnq 6946	. . . . . . . . . . . . 13 |- ( x e. Q. -> ( x .Q 1Q ) = x )
72	71	adantr 270	. . . . . . . . . . . 12 |- ( ( x e. Q. /\ f e. Q. ) -> ( x .Q 1Q ) = x )
73	68, 70, 72	3eqtrrd 2125	. . . . . . . . . . 11 |- ( ( x e. Q. /\ f e. Q. ) -> x = ( f .Q ( x .Q ( *Q ` f ) ) ) )
74	43, 73	syl 14	. . . . . . . . . 10 |- ( x <Q f -> x = ( f .Q ( x .Q ( *Q ` f ) ) ) )
75		oveq2 5660	. . . . . . . . . . . 12 |- ( g = ( x .Q ( *Q ` f ) ) -> ( f .Q g ) = ( f .Q ( x .Q ( *Q ` f ) ) ) )
76	75	eqeq2d 2099	. . . . . . . . . . 11 |- ( g = ( x .Q ( *Q ` f ) ) -> ( x = ( f .Q g ) <-> x = ( f .Q ( x .Q ( *Q ` f ) ) ) ) )
77	76	rspcev 2722	. . . . . . . . . 10 |- ( ( ( x .Q ( *Q ` f ) ) e. ( 1st ` 1P ) /\ x = ( f .Q ( x .Q ( *Q ` f ) ) ) ) -> E. g e. ( 1st ` 1P ) x = ( f .Q g ) )
78	65, 74, 77	syl2anc 403	. . . . . . . . 9 |- ( x <Q f -> E. g e. ( 1st ` 1P ) x = ( f .Q g ) )
79	78	a1i 9	. . . . . . . 8 |- ( f e. ( 1st ` A ) -> ( x <Q f -> E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) )
80	79	ancld 318	. . . . . . 7 |- ( f e. ( 1st ` A ) -> ( x <Q f -> ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) ) )
81	80	reximia 2468	. . . . . 6 |- ( E. f e. ( 1st ` A ) x <Q f -> E. f e. ( 1st ` A ) ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) )
82	41, 81	syl 14	. . . . 5 |- ( ( A e. P. /\ x e. ( 1st ` A ) ) -> E. f e. ( 1st ` A ) ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) )
83	82	ex 113	. . . 4 |- ( A e. P. -> ( x e. ( 1st ` A ) -> E. f e. ( 1st ` A ) ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) ) )
84		prcdnql 7041	. . . . . . 7 |- ( ( <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. /\ f e. ( 1st ` A ) ) -> ( x <Q f -> x e. ( 1st ` A ) ) )
85	10, 84	sylan 277	. . . . . 6 |- ( ( A e. P. /\ f e. ( 1st ` A ) ) -> ( x <Q f -> x e. ( 1st ` A ) ) )
86	85	adantrd 273	. . . . 5 |- ( ( A e. P. /\ f e. ( 1st ` A ) ) -> ( ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) -> x e. ( 1st ` A ) ) )
87	86	rexlimdva 2489	. . . 4 |- ( A e. P. -> ( E. f e. ( 1st ` A ) ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) -> x e. ( 1st ` A ) ) )
88	83, 87	impbid 127	. . 3 |- ( A e. P. -> ( x e. ( 1st ` A ) <-> E. f e. ( 1st ` A ) ( x <Q f /\ E. g e. ( 1st ` 1P ) x = ( f .Q g ) ) ) )
89	35, 39, 88	3bitr4d 218	. 2 |- ( A e. P. -> ( x e. ( 1st ` ( A .P. 1P ) ) <-> x e. ( 1st ` A ) ) )
90	89	eqrdv 2086	1 |- ( A e. P. -> ( 1st ` ( A .P. 1P ) ) = ( 1st ` A ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   /\ w3a 924   = wceq 1289   e. wcel 1438   E.wrex 2360   C_ wss 2999   <.cop 3449   class class class wbr 3845   ` cfv 5015  (class class class)co 5652   1stc1st 5909   2ndc2nd 5910   Q.cnq 6837   1Qc1q 6838   .Q cmq 6840   *Qcrq 6841   <Q cltq 6842   P.cnp 6848   1Pc1p 6849   .P. cmp 6851

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3954  ax-sep 3957  ax-nul 3965  ax-pow 4009  ax-pr 4036  ax-un 4260  ax-setind 4353  ax-iinf 4403

This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-int 3689  df-iun 3732  df-br 3846  df-opab 3900  df-mpt 3901  df-tr 3937  df-eprel 4116  df-id 4120  df-po 4123  df-iso 4124  df-iord 4193  df-on 4195  df-suc 4198  df-iom 4406  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-res 4450  df-ima 4451  df-iota 4980  df-fun 5017  df-fn 5018  df-f 5019  df-f1 5020  df-fo 5021  df-f1o 5022  df-fv 5023  df-ov 5655  df-oprab 5656  df-mpt2 5657  df-1st 5911  df-2nd 5912  df-recs 6070  df-irdg 6135  df-1o 6181  df-oadd 6185  df-omul 6186  df-er 6290  df-ec 6292  df-qs 6296  df-ni 6861  df-pli 6862  df-mi 6863  df-lti 6864  df-plpq 6901  df-mpq 6902  df-enq 6904  df-nqqs 6905  df-plqqs 6906  df-mqqs 6907  df-1nqqs 6908  df-rq 6909  df-ltnqqs 6910  df-inp 7023  df-i1p 7024  df-imp 7026

This theorem is referenced by:  1idpr  7149