1idprl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer	< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 1idprl		Structured version GIF version

Theorem 1idprl 6564

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

**Assertion**
Ref	Expression
1idprl	⊢ (A ∈ P → (1^st ‘(A ·_P 1_P)) = (1^st ‘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 2958	. . . . . 6 ⊢ (1^st ‘1_P) ⊆ (1^st ‘1_P)
2		rexss 3001	. . . . . 6 ⊢ ((1^st ‘1_P) ⊆ (1^st ‘1_P) → (∃g ∈ (1^st ‘1_P)x = (f ·_Q g) ↔ ∃g ∈ (1^st ‘1_P)(g ∈ (1^st ‘1_P) ∧ x = (f ·_Q g))))
3	1, 2	ax-mp 7	. . . . 5 ⊢ (∃g ∈ (1^st ‘1_P)x = (f ·_Q g) ↔ ∃g ∈ (1^st ‘1_P)(g ∈ (1^st ‘1_P) ∧ x = (f ·_Q g)))
4		r19.42v 2461	. . . . . 6 ⊢ (∃g ∈ (1^st ‘1_P)(x <_Q f ∧ x = (f ·_Q g)) ↔ (x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g)))
5		1pr 6534	. . . . . . . . . . 11 ⊢ 1_P ∈ P
6		prop 6457	. . . . . . . . . . . 12 ⊢ (1_P ∈ P → ⟨(1^st ‘1_P), (2^nd ‘1_P)⟩ ∈ P)
7		elprnql 6463	. . . . . . . . . . . 12 ⊢ ((⟨(1^st ‘1_P), (2^nd ‘1_P)⟩ ∈ P ∧ g ∈ (1^st ‘1_P)) → g ∈ Q)
8	6, 7	sylan 267	. . . . . . . . . . 11 ⊢ ((1_P ∈ P ∧ g ∈ (1^st ‘1_P)) → g ∈ Q)
9	5, 8	mpan 400	. . . . . . . . . 10 ⊢ (g ∈ (1^st ‘1_P) → g ∈ Q)
10		prop 6457	. . . . . . . . . . . 12 ⊢ (A ∈ P → ⟨(1^st ‘A), (2^nd ‘A)⟩ ∈ P)
11		elprnql 6463	. . . . . . . . . . . 12 ⊢ ((⟨(1^st ‘A), (2^nd ‘A)⟩ ∈ P ∧ f ∈ (1^st ‘A)) → f ∈ Q)
12	10, 11	sylan 267	. . . . . . . . . . 11 ⊢ ((A ∈ P ∧ f ∈ (1^st ‘A)) → f ∈ Q)
13		breq1 3758	. . . . . . . . . . . . 13 ⊢ (x = (f ·_Q g) → (x <_Q f ↔ (f ·_Q g) <_Q f))
14	13	3ad2ant3 926	. . . . . . . . . . . 12 ⊢ ((f ∈ Q ∧ g ∈ Q ∧ x = (f ·_Q g)) → (x <_Q f ↔ (f ·_Q g) <_Q f))
15		1prl 6535	. . . . . . . . . . . . . . 15 ⊢ (1^st ‘1_P) = {g ∣ g <_Q 1_Q}
16	15	abeq2i 2145	. . . . . . . . . . . . . 14 ⊢ (g ∈ (1^st ‘1_P) ↔ g <_Q 1_Q)
17		1nq 6350	. . . . . . . . . . . . . . . . 17 ⊢ 1_Q ∈ Q
18		ltmnqg 6385	. . . . . . . . . . . . . . . . 17 ⊢ ((g ∈ Q ∧ 1_Q ∈ Q ∧ f ∈ Q) → (g <_Q 1_Q ↔ (f ·_Q g) <_Q (f ·_Q 1_Q)))
19	17, 18	mp3an2 1219	. . . . . . . . . . . . . . . 16 ⊢ ((g ∈ Q ∧ f ∈ Q) → (g <_Q 1_Q ↔ (f ·_Q g) <_Q (f ·_Q 1_Q)))
20	19	ancoms 255	. . . . . . . . . . . . . . 15 ⊢ ((f ∈ Q ∧ g ∈ Q) → (g <_Q 1_Q ↔ (f ·_Q g) <_Q (f ·_Q 1_Q)))
21		mulidnq 6373	. . . . . . . . . . . . . . . . 17 ⊢ (f ∈ Q → (f ·_Q 1_Q) = f)
22	21	breq2d 3767	. . . . . . . . . . . . . . . 16 ⊢ (f ∈ Q → ((f ·_Q g) <_Q (f ·_Q 1_Q) ↔ (f ·_Q g) <_Q f))
23	22	adantr 261	. . . . . . . . . . . . . . 15 ⊢ ((f ∈ Q ∧ g ∈ Q) → ((f ·_Q g) <_Q (f ·_Q 1_Q) ↔ (f ·_Q g) <_Q f))
24	20, 23	bitrd 177	. . . . . . . . . . . . . 14 ⊢ ((f ∈ Q ∧ g ∈ Q) → (g <_Q 1_Q ↔ (f ·_Q g) <_Q f))
25	16, 24	syl5rbb 182	. . . . . . . . . . . . 13 ⊢ ((f ∈ Q ∧ g ∈ Q) → ((f ·_Q g) <_Q f ↔ g ∈ (1^st ‘1_P)))
26	25	3adant3 923	. . . . . . . . . . . 12 ⊢ ((f ∈ Q ∧ g ∈ Q ∧ x = (f ·_Q g)) → ((f ·_Q g) <_Q f ↔ g ∈ (1^st ‘1_P)))
27	14, 26	bitrd 177	. . . . . . . . . . 11 ⊢ ((f ∈ Q ∧ g ∈ Q ∧ x = (f ·_Q g)) → (x <_Q f ↔ g ∈ (1^st ‘1_P)))
28	12, 27	syl3an1 1167	. . . . . . . . . 10 ⊢ (((A ∈ P ∧ f ∈ (1^st ‘A)) ∧ g ∈ Q ∧ x = (f ·_Q g)) → (x <_Q f ↔ g ∈ (1^st ‘1_P)))
29	9, 28	syl3an2 1168	. . . . . . . . 9 ⊢ (((A ∈ P ∧ f ∈ (1^st ‘A)) ∧ g ∈ (1^st ‘1_P) ∧ x = (f ·_Q g)) → (x <_Q f ↔ g ∈ (1^st ‘1_P)))
30	29	3expia 1105	. . . . . . . 8 ⊢ (((A ∈ P ∧ f ∈ (1^st ‘A)) ∧ g ∈ (1^st ‘1_P)) → (x = (f ·_Q g) → (x <_Q f ↔ g ∈ (1^st ‘1_P))))
31	30	pm5.32rd 424	. . . . . . 7 ⊢ (((A ∈ P ∧ f ∈ (1^st ‘A)) ∧ g ∈ (1^st ‘1_P)) → ((x <_Q f ∧ x = (f ·_Q g)) ↔ (g ∈ (1^st ‘1_P) ∧ x = (f ·_Q g))))
32	31	rexbidva 2317	. . . . . 6 ⊢ ((A ∈ P ∧ f ∈ (1^st ‘A)) → (∃g ∈ (1^st ‘1_P)(x <_Q f ∧ x = (f ·_Q g)) ↔ ∃g ∈ (1^st ‘1_P)(g ∈ (1^st ‘1_P) ∧ x = (f ·_Q g))))
33	4, 32	syl5rbbr 184	. . . . 5 ⊢ ((A ∈ P ∧ f ∈ (1^st ‘A)) → (∃g ∈ (1^st ‘1_P)(g ∈ (1^st ‘1_P) ∧ x = (f ·_Q g)) ↔ (x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g))))
34	3, 33	syl5bb 181	. . . 4 ⊢ ((A ∈ P ∧ f ∈ (1^st ‘A)) → (∃g ∈ (1^st ‘1_P)x = (f ·_Q g) ↔ (x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g))))
35	34	rexbidva 2317	. . 3 ⊢ (A ∈ P → (∃f ∈ (1^st ‘A)∃g ∈ (1^st ‘1_P)x = (f ·_Q g) ↔ ∃f ∈ (1^st ‘A)(x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g))))
36		df-imp 6451	. . . . 5 ⊢ ·_P = (y ∈ P, z ∈ P ↦ ⟨{w ∈ Q ∣ ∃u ∈ Q ∃v ∈ Q (u ∈ (1^st ‘y) ∧ v ∈ (1^st ‘z) ∧ w = (u ·_Q v))}, {w ∈ Q ∣ ∃u ∈ Q ∃v ∈ Q (u ∈ (2^nd ‘y) ∧ v ∈ (2^nd ‘z) ∧ w = (u ·_Q v))}⟩)
37		mulclnq 6360	. . . . 5 ⊢ ((u ∈ Q ∧ v ∈ Q) → (u ·_Q v) ∈ Q)
38	36, 37	genpelvl 6494	. . . 4 ⊢ ((A ∈ P ∧ 1_P ∈ P) → (x ∈ (1^st ‘(A ·_P 1_P)) ↔ ∃f ∈ (1^st ‘A)∃g ∈ (1^st ‘1_P)x = (f ·_Q g)))
39	5, 38	mpan2 401	. . 3 ⊢ (A ∈ P → (x ∈ (1^st ‘(A ·_P 1_P)) ↔ ∃f ∈ (1^st ‘A)∃g ∈ (1^st ‘1_P)x = (f ·_Q g)))
40		prnmaxl 6470	. . . . . . 7 ⊢ ((⟨(1^st ‘A), (2^nd ‘A)⟩ ∈ P ∧ x ∈ (1^st ‘A)) → ∃f ∈ (1^st ‘A)x <_Q f)
41	10, 40	sylan 267	. . . . . 6 ⊢ ((A ∈ P ∧ x ∈ (1^st ‘A)) → ∃f ∈ (1^st ‘A)x <_Q f)
42		ltrelnq 6349	. . . . . . . . . . . . 13 ⊢ <_Q ⊆ (Q × Q)
43	42	brel 4335	. . . . . . . . . . . 12 ⊢ (x <_Q f → (x ∈ Q ∧ f ∈ Q))
44		ltmnqg 6385	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ Q ∧ z ∈ Q ∧ w ∈ Q) → (y <_Q z ↔ (w ·_Q y) <_Q (w ·_Q z)))
45	44	adantl 262	. . . . . . . . . . . . . . 15 ⊢ (((x ∈ Q ∧ f ∈ Q) ∧ (y ∈ Q ∧ z ∈ Q ∧ w ∈ Q)) → (y <_Q z ↔ (w ·_Q y) <_Q (w ·_Q z)))
46		simpl 102	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ Q ∧ f ∈ Q) → x ∈ Q)
47		simpr 103	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ Q ∧ f ∈ Q) → f ∈ Q)
48		recclnq 6376	. . . . . . . . . . . . . . . 16 ⊢ (f ∈ Q → (*_Q‘f) ∈ Q)
49	48	adantl 262	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ Q ∧ f ∈ Q) → (*_Q‘f) ∈ Q)
50		mulcomnqg 6367	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ Q ∧ z ∈ Q) → (y ·_Q z) = (z ·_Q y))
51	50	adantl 262	. . . . . . . . . . . . . . 15 ⊢ (((x ∈ Q ∧ f ∈ Q) ∧ (y ∈ Q ∧ z ∈ Q)) → (y ·_Q z) = (z ·_Q y))
52	45, 46, 47, 49, 51	caovord2d 5612	. . . . . . . . . . . . . 14 ⊢ ((x ∈ Q ∧ f ∈ Q) → (x <_Q f ↔ (x ·_Q (_Q‘f)) <_Q (f ·_Q (_Q‘f))))
53		recidnq 6377	. . . . . . . . . . . . . . . 16 ⊢ (f ∈ Q → (f ·_Q (*_Q‘f)) = 1_Q)
54	53	breq2d 3767	. . . . . . . . . . . . . . 15 ⊢ (f ∈ Q → ((x ·_Q (_Q‘f)) <_Q (f ·_Q (_Q‘f)) ↔ (x ·_Q (*_Q‘f)) <_Q 1_Q))
55	54	adantl 262	. . . . . . . . . . . . . 14 ⊢ ((x ∈ Q ∧ f ∈ Q) → ((x ·_Q (_Q‘f)) <_Q (f ·_Q (_Q‘f)) ↔ (x ·_Q (*_Q‘f)) <_Q 1_Q))
56	52, 55	bitrd 177	. . . . . . . . . . . . 13 ⊢ ((x ∈ Q ∧ f ∈ Q) → (x <_Q f ↔ (x ·_Q (*_Q‘f)) <_Q 1_Q))
57	56	biimpd 132	. . . . . . . . . . . 12 ⊢ ((x ∈ Q ∧ f ∈ Q) → (x <_Q f → (x ·_Q (*_Q‘f)) <_Q 1_Q))
58	43, 57	mpcom 32	. . . . . . . . . . 11 ⊢ (x <_Q f → (x ·_Q (*_Q‘f)) <_Q 1_Q)
59		mulclnq 6360	. . . . . . . . . . . . . 14 ⊢ ((x ∈ Q ∧ (_Q‘f) ∈ Q) → (x ·_Q (_Q‘f)) ∈ Q)
60	48, 59	sylan2 270	. . . . . . . . . . . . 13 ⊢ ((x ∈ Q ∧ f ∈ Q) → (x ·_Q (*_Q‘f)) ∈ Q)
61	43, 60	syl 14	. . . . . . . . . . . 12 ⊢ (x <_Q f → (x ·_Q (*_Q‘f)) ∈ Q)
62		breq1 3758	. . . . . . . . . . . . 13 ⊢ (g = (x ·_Q (_Q‘f)) → (g <_Q 1_Q ↔ (x ·_Q (_Q‘f)) <_Q 1_Q))
63	62, 15	elab2g 2683	. . . . . . . . . . . 12 ⊢ ((x ·_Q (_Q‘f)) ∈ Q → ((x ·_Q (_Q‘f)) ∈ (1^st ‘1_P) ↔ (x ·_Q (*_Q‘f)) <_Q 1_Q))
64	61, 63	syl 14	. . . . . . . . . . 11 ⊢ (x <_Q f → ((x ·_Q (_Q‘f)) ∈ (1^st ‘1_P) ↔ (x ·_Q (_Q‘f)) <_Q 1_Q))
65	58, 64	mpbird 156	. . . . . . . . . 10 ⊢ (x <_Q f → (x ·_Q (*_Q‘f)) ∈ (1^st ‘1_P))
66		mulassnqg 6368	. . . . . . . . . . . . . 14 ⊢ ((y ∈ Q ∧ z ∈ Q ∧ w ∈ Q) → ((y ·_Q z) ·_Q w) = (y ·_Q (z ·_Q w)))
67	66	adantl 262	. . . . . . . . . . . . 13 ⊢ (((x ∈ Q ∧ f ∈ Q) ∧ (y ∈ Q ∧ z ∈ Q ∧ w ∈ Q)) → ((y ·_Q z) ·_Q w) = (y ·_Q (z ·_Q w)))
68	47, 46, 49, 51, 67	caov12d 5624	. . . . . . . . . . . 12 ⊢ ((x ∈ Q ∧ f ∈ Q) → (f ·_Q (x ·_Q (_Q‘f))) = (x ·_Q (f ·_Q (_Q‘f))))
69	53	oveq2d 5471	. . . . . . . . . . . . 13 ⊢ (f ∈ Q → (x ·_Q (f ·_Q (*_Q‘f))) = (x ·_Q 1_Q))
70	69	adantl 262	. . . . . . . . . . . 12 ⊢ ((x ∈ Q ∧ f ∈ Q) → (x ·_Q (f ·_Q (*_Q‘f))) = (x ·_Q 1_Q))
71		mulidnq 6373	. . . . . . . . . . . . 13 ⊢ (x ∈ Q → (x ·_Q 1_Q) = x)
72	71	adantr 261	. . . . . . . . . . . 12 ⊢ ((x ∈ Q ∧ f ∈ Q) → (x ·_Q 1_Q) = x)
73	68, 70, 72	3eqtrrd 2074	. . . . . . . . . . 11 ⊢ ((x ∈ Q ∧ f ∈ 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 5463	. . . . . . . . . . . 12 ⊢ (g = (x ·_Q (_Q‘f)) → (f ·_Q g) = (f ·_Q (x ·_Q (_Q‘f))))
76	75	eqeq2d 2048	. . . . . . . . . . 11 ⊢ (g = (x ·_Q (_Q‘f)) → (x = (f ·_Q g) ↔ x = (f ·_Q (x ·_Q (_Q‘f)))))
77	76	rspcev 2650	. . . . . . . . . 10 ⊢ (((x ·_Q (_Q‘f)) ∈ (1^st ‘1_P) ∧ x = (f ·_Q (x ·_Q (_Q‘f)))) → ∃g ∈ (1^st ‘1_P)x = (f ·_Q g))
78	65, 74, 77	syl2anc 391	. . . . . . . . 9 ⊢ (x <_Q f → ∃g ∈ (1^st ‘1_P)x = (f ·_Q g))
79	78	a1i 9	. . . . . . . 8 ⊢ (f ∈ (1^st ‘A) → (x <_Q f → ∃g ∈ (1^st ‘1_P)x = (f ·_Q g)))
80	79	ancld 308	. . . . . . 7 ⊢ (f ∈ (1^st ‘A) → (x <_Q f → (x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g))))
81	80	reximia 2408	. . . . . 6 ⊢ (∃f ∈ (1^st ‘A)x <_Q f → ∃f ∈ (1^st ‘A)(x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g)))
82	41, 81	syl 14	. . . . 5 ⊢ ((A ∈ P ∧ x ∈ (1^st ‘A)) → ∃f ∈ (1^st ‘A)(x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g)))
83	82	ex 108	. . . 4 ⊢ (A ∈ P → (x ∈ (1^st ‘A) → ∃f ∈ (1^st ‘A)(x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g))))
84		prcdnql 6466	. . . . . . 7 ⊢ ((⟨(1^st ‘A), (2^nd ‘A)⟩ ∈ P ∧ f ∈ (1^st ‘A)) → (x <_Q f → x ∈ (1^st ‘A)))
85	10, 84	sylan 267	. . . . . 6 ⊢ ((A ∈ P ∧ f ∈ (1^st ‘A)) → (x <_Q f → x ∈ (1^st ‘A)))
86	85	adantrd 264	. . . . 5 ⊢ ((A ∈ P ∧ f ∈ (1^st ‘A)) → ((x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g)) → x ∈ (1^st ‘A)))
87	86	rexlimdva 2427	. . . 4 ⊢ (A ∈ P → (∃f ∈ (1^st ‘A)(x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g)) → x ∈ (1^st ‘A)))
88	83, 87	impbid 120	. . 3 ⊢ (A ∈ P → (x ∈ (1^st ‘A) ↔ ∃f ∈ (1^st ‘A)(x <_Q f ∧ ∃g ∈ (1^st ‘1_P)x = (f ·_Q g))))
89	35, 39, 88	3bitr4d 209	. 2 ⊢ (A ∈ P → (x ∈ (1^st ‘(A ·_P 1_P)) ↔ x ∈ (1^st ‘A)))
90	89	eqrdv 2035	1 ⊢ (A ∈ P → (1^st ‘(A ·_P 1_P)) = (1^st ‘A))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 ∧ w3a 884 = wceq 1242 ∈ wcel 1390 ∃wrex 2301 ⊆ wss 2911 ⟨cop 3370 class class class wbr 3755 ‘cfv 4845 (class class class)co 5455 1^st c1st 5707 2^nd c2nd 5708 Qcnq 6264 1_Qc1q 6265 ·_Q cmq 6267 *_Qcrq 6268 <_Q cltq 6269 Pcnp 6275 1_Pc1p 6276 ·_P cmp 6278

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bnd 1396 ax-4 1397 ax-13 1401 ax-14 1402 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 ax-coll 3863 ax-sep 3866 ax-nul 3874 ax-pow 3918 ax-pr 3935 ax-un 4136 ax-setind 4220 ax-iinf 4254

This theorem depends on definitions: df-bi 110 df-dc 742 df-3or 885 df-3an 886 df-tru 1245 df-fal 1248 df-nf 1347 df-sb 1643 df-eu 1900 df-mo 1901 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ne 2203 df-ral 2305 df-rex 2306 df-reu 2307 df-rab 2309 df-v 2553 df-sbc 2759 df-csb 2847 df-dif 2914 df-un 2916 df-in 2918 df-ss 2925 df-nul 3219 df-pw 3353 df-sn 3373 df-pr 3374 df-op 3376 df-uni 3572 df-int 3607 df-iun 3650 df-br 3756 df-opab 3810 df-mpt 3811 df-tr 3846 df-eprel 4017 df-id 4021 df-po 4024 df-iso 4025 df-iord 4069 df-on 4071 df-suc 4074 df-iom 4257 df-xp 4294 df-rel 4295 df-cnv 4296 df-co 4297 df-dm 4298 df-rn 4299 df-res 4300 df-ima 4301 df-iota 4810 df-fun 4847 df-fn 4848 df-f 4849 df-f1 4850 df-fo 4851 df-f1o 4852 df-fv 4853 df-ov 5458 df-oprab 5459 df-mpt2 5460 df-1st 5709 df-2nd 5710 df-recs 5861 df-irdg 5897 df-1o 5940 df-oadd 5944 df-omul 5945 df-er 6042 df-ec 6044 df-qs 6048 df-ni 6288 df-pli 6289 df-mi 6290 df-lti 6291 df-plpq 6328 df-mpq 6329 df-enq 6331 df-nqqs 6332 df-plqqs 6333 df-mqqs 6334 df-1nqqs 6335 df-rq 6336 df-ltnqqs 6337 df-inp 6448 df-i1p 6449 df-imp 6451

This theorem is referenced by: 1idpr 6566

W3C validator