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

Theorem 1idpru 6567
 Description: Lemma for 1idpr 6568. (Contributed by Jim Kingdon, 13-Dec-2019.)
Assertion
Ref Expression
1idpru (A P → (2nd ‘(A ·P 1P)) = (2ndA))

Proof of Theorem 1idpru
Dummy variables x y z w v u f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 2958 . . . . . 6 (2nd ‘1P) ⊆ (2nd ‘1P)
2 rexss 3001 . . . . . 6 ((2nd ‘1P) ⊆ (2nd ‘1P) → ( (2nd ‘1P)x = (f ·Q ) ↔ (2nd ‘1P)( (2nd ‘1P) x = (f ·Q ))))
31, 2ax-mp 7 . . . . 5 ( (2nd ‘1P)x = (f ·Q ) ↔ (2nd ‘1P)( (2nd ‘1P) x = (f ·Q )))
4 r19.42v 2461 . . . . . 6 ( (2nd ‘1P)(f <Q x x = (f ·Q )) ↔ (f <Q x (2nd ‘1P)x = (f ·Q )))
5 1pr 6535 . . . . . . . . . . 11 1P P
6 prop 6458 . . . . . . . . . . . 12 (1P P → ⟨(1st ‘1P), (2nd ‘1P)⟩ P)
7 elprnqu 6465 . . . . . . . . . . . 12 ((⟨(1st ‘1P), (2nd ‘1P)⟩ P (2nd ‘1P)) → Q)
86, 7sylan 267 . . . . . . . . . . 11 ((1P P (2nd ‘1P)) → Q)
95, 8mpan 400 . . . . . . . . . 10 ( (2nd ‘1P) → Q)
10 prop 6458 . . . . . . . . . . . 12 (A P → ⟨(1stA), (2ndA)⟩ P)
11 elprnqu 6465 . . . . . . . . . . . 12 ((⟨(1stA), (2ndA)⟩ P f (2ndA)) → f Q)
1210, 11sylan 267 . . . . . . . . . . 11 ((A P f (2ndA)) → f Q)
13 breq2 3759 . . . . . . . . . . . . 13 (x = (f ·Q ) → (f <Q xf <Q (f ·Q )))
14133ad2ant3 926 . . . . . . . . . . . 12 ((f Q Q x = (f ·Q )) → (f <Q xf <Q (f ·Q )))
15 1pru 6537 . . . . . . . . . . . . . . 15 (2nd ‘1P) = { ∣ 1Q <Q }
1615abeq2i 2145 . . . . . . . . . . . . . 14 ( (2nd ‘1P) ↔ 1Q <Q )
17 1nq 6350 . . . . . . . . . . . . . . . . 17 1Q Q
18 ltmnqg 6385 . . . . . . . . . . . . . . . . 17 ((1Q Q Q f Q) → (1Q <Q ↔ (f ·Q 1Q) <Q (f ·Q )))
1917, 18mp3an1 1218 . . . . . . . . . . . . . . . 16 (( Q f Q) → (1Q <Q ↔ (f ·Q 1Q) <Q (f ·Q )))
2019ancoms 255 . . . . . . . . . . . . . . 15 ((f Q Q) → (1Q <Q ↔ (f ·Q 1Q) <Q (f ·Q )))
21 mulidnq 6373 . . . . . . . . . . . . . . . . 17 (f Q → (f ·Q 1Q) = f)
2221breq1d 3765 . . . . . . . . . . . . . . . 16 (f Q → ((f ·Q 1Q) <Q (f ·Q ) ↔ f <Q (f ·Q )))
2322adantr 261 . . . . . . . . . . . . . . 15 ((f Q Q) → ((f ·Q 1Q) <Q (f ·Q ) ↔ f <Q (f ·Q )))
2420, 23bitrd 177 . . . . . . . . . . . . . 14 ((f Q Q) → (1Q <Q f <Q (f ·Q )))
2516, 24syl5rbb 182 . . . . . . . . . . . . 13 ((f Q Q) → (f <Q (f ·Q ) ↔ (2nd ‘1P)))
26253adant3 923 . . . . . . . . . . . 12 ((f Q Q x = (f ·Q )) → (f <Q (f ·Q ) ↔ (2nd ‘1P)))
2714, 26bitrd 177 . . . . . . . . . . 11 ((f Q Q x = (f ·Q )) → (f <Q x (2nd ‘1P)))
2812, 27syl3an1 1167 . . . . . . . . . 10 (((A P f (2ndA)) Q x = (f ·Q )) → (f <Q x (2nd ‘1P)))
299, 28syl3an2 1168 . . . . . . . . 9 (((A P f (2ndA)) (2nd ‘1P) x = (f ·Q )) → (f <Q x (2nd ‘1P)))
30293expia 1105 . . . . . . . 8 (((A P f (2ndA)) (2nd ‘1P)) → (x = (f ·Q ) → (f <Q x (2nd ‘1P))))
3130pm5.32rd 424 . . . . . . 7 (((A P f (2ndA)) (2nd ‘1P)) → ((f <Q x x = (f ·Q )) ↔ ( (2nd ‘1P) x = (f ·Q ))))
3231rexbidva 2317 . . . . . 6 ((A P f (2ndA)) → ( (2nd ‘1P)(f <Q x x = (f ·Q )) ↔ (2nd ‘1P)( (2nd ‘1P) x = (f ·Q ))))
334, 32syl5rbbr 184 . . . . 5 ((A P f (2ndA)) → ( (2nd ‘1P)( (2nd ‘1P) x = (f ·Q )) ↔ (f <Q x (2nd ‘1P)x = (f ·Q ))))
343, 33syl5bb 181 . . . 4 ((A P f (2ndA)) → ( (2nd ‘1P)x = (f ·Q ) ↔ (f <Q x (2nd ‘1P)x = (f ·Q ))))
3534rexbidva 2317 . . 3 (A P → (f (2ndA) (2nd ‘1P)x = (f ·Q ) ↔ f (2ndA)(f <Q x (2nd ‘1P)x = (f ·Q ))))
36 df-imp 6452 . . . . 5 ·P = (y P, z P ↦ ⟨{w Qu Q v Q (u (1sty) v (1stz) w = (u ·Q v))}, {w Qu Q v Q (u (2ndy) v (2ndz) w = (u ·Q v))}⟩)
37 mulclnq 6360 . . . . 5 ((u Q v Q) → (u ·Q v) Q)
3836, 37genpelvu 6496 . . . 4 ((A P 1P P) → (x (2nd ‘(A ·P 1P)) ↔ f (2ndA) (2nd ‘1P)x = (f ·Q )))
395, 38mpan2 401 . . 3 (A P → (x (2nd ‘(A ·P 1P)) ↔ f (2ndA) (2nd ‘1P)x = (f ·Q )))
40 prnminu 6472 . . . . . . 7 ((⟨(1stA), (2ndA)⟩ P x (2ndA)) → f (2ndA)f <Q x)
4110, 40sylan 267 . . . . . 6 ((A P x (2ndA)) → f (2ndA)f <Q x)
42 ltrelnq 6349 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
4342brel 4335 . . . . . . . . . . . . 13 (f <Q x → (f Q x Q))
4443ancomd 254 . . . . . . . . . . . 12 (f <Q x → (x Q f Q))
45 ltmnqg 6385 . . . . . . . . . . . . . . . 16 ((y Q z Q w Q) → (y <Q z ↔ (w ·Q y) <Q (w ·Q z)))
4645adantl 262 . . . . . . . . . . . . . . 15 (((x Q f Q) (y Q z Q w Q)) → (y <Q z ↔ (w ·Q y) <Q (w ·Q z)))
47 simpr 103 . . . . . . . . . . . . . . 15 ((x Q f Q) → f Q)
48 simpl 102 . . . . . . . . . . . . . . 15 ((x Q f Q) → x Q)
49 recclnq 6376 . . . . . . . . . . . . . . . 16 (f Q → (*Qf) Q)
5049adantl 262 . . . . . . . . . . . . . . 15 ((x Q f Q) → (*Qf) Q)
51 mulcomnqg 6367 . . . . . . . . . . . . . . . 16 ((y Q z Q) → (y ·Q z) = (z ·Q y))
5251adantl 262 . . . . . . . . . . . . . . 15 (((x Q f Q) (y Q z Q)) → (y ·Q z) = (z ·Q y))
5346, 47, 48, 50, 52caovord2d 5612 . . . . . . . . . . . . . 14 ((x Q f Q) → (f <Q x ↔ (f ·Q (*Qf)) <Q (x ·Q (*Qf))))
54 recidnq 6377 . . . . . . . . . . . . . . . 16 (f Q → (f ·Q (*Qf)) = 1Q)
5554breq1d 3765 . . . . . . . . . . . . . . 15 (f Q → ((f ·Q (*Qf)) <Q (x ·Q (*Qf)) ↔ 1Q <Q (x ·Q (*Qf))))
5655adantl 262 . . . . . . . . . . . . . 14 ((x Q f Q) → ((f ·Q (*Qf)) <Q (x ·Q (*Qf)) ↔ 1Q <Q (x ·Q (*Qf))))
5753, 56bitrd 177 . . . . . . . . . . . . 13 ((x Q f Q) → (f <Q x ↔ 1Q <Q (x ·Q (*Qf))))
5857biimpd 132 . . . . . . . . . . . 12 ((x Q f Q) → (f <Q x → 1Q <Q (x ·Q (*Qf))))
5944, 58mpcom 32 . . . . . . . . . . 11 (f <Q x → 1Q <Q (x ·Q (*Qf)))
60 mulclnq 6360 . . . . . . . . . . . . 13 ((x Q (*Qf) Q) → (x ·Q (*Qf)) Q)
6149, 60sylan2 270 . . . . . . . . . . . 12 ((x Q f Q) → (x ·Q (*Qf)) Q)
62 breq2 3759 . . . . . . . . . . . . 13 ( = (x ·Q (*Qf)) → (1Q <Q ↔ 1Q <Q (x ·Q (*Qf))))
6362, 15elab2g 2683 . . . . . . . . . . . 12 ((x ·Q (*Qf)) Q → ((x ·Q (*Qf)) (2nd ‘1P) ↔ 1Q <Q (x ·Q (*Qf))))
6444, 61, 633syl 17 . . . . . . . . . . 11 (f <Q x → ((x ·Q (*Qf)) (2nd ‘1P) ↔ 1Q <Q (x ·Q (*Qf))))
6559, 64mpbird 156 . . . . . . . . . 10 (f <Q x → (x ·Q (*Qf)) (2nd ‘1P))
66 mulassnqg 6368 . . . . . . . . . . . . . 14 ((y Q z Q w Q) → ((y ·Q z) ·Q w) = (y ·Q (z ·Q w)))
6766adantl 262 . . . . . . . . . . . . 13 (((x Q f Q) (y Q z Q w Q)) → ((y ·Q z) ·Q w) = (y ·Q (z ·Q w)))
6847, 48, 50, 52, 67caov12d 5624 . . . . . . . . . . . 12 ((x Q f Q) → (f ·Q (x ·Q (*Qf))) = (x ·Q (f ·Q (*Qf))))
6954oveq2d 5471 . . . . . . . . . . . . 13 (f Q → (x ·Q (f ·Q (*Qf))) = (x ·Q 1Q))
7069adantl 262 . . . . . . . . . . . 12 ((x Q f Q) → (x ·Q (f ·Q (*Qf))) = (x ·Q 1Q))
71 mulidnq 6373 . . . . . . . . . . . . 13 (x Q → (x ·Q 1Q) = x)
7271adantr 261 . . . . . . . . . . . 12 ((x Q f Q) → (x ·Q 1Q) = x)
7368, 70, 723eqtrrd 2074 . . . . . . . . . . 11 ((x Q f Q) → x = (f ·Q (x ·Q (*Qf))))
7444, 73syl 14 . . . . . . . . . 10 (f <Q xx = (f ·Q (x ·Q (*Qf))))
75 oveq2 5463 . . . . . . . . . . . 12 ( = (x ·Q (*Qf)) → (f ·Q ) = (f ·Q (x ·Q (*Qf))))
7675eqeq2d 2048 . . . . . . . . . . 11 ( = (x ·Q (*Qf)) → (x = (f ·Q ) ↔ x = (f ·Q (x ·Q (*Qf)))))
7776rspcev 2650 . . . . . . . . . 10 (((x ·Q (*Qf)) (2nd ‘1P) x = (f ·Q (x ·Q (*Qf)))) → (2nd ‘1P)x = (f ·Q ))
7865, 74, 77syl2anc 391 . . . . . . . . 9 (f <Q x (2nd ‘1P)x = (f ·Q ))
7978a1i 9 . . . . . . . 8 (f (2ndA) → (f <Q x (2nd ‘1P)x = (f ·Q )))
8079ancld 308 . . . . . . 7 (f (2ndA) → (f <Q x → (f <Q x (2nd ‘1P)x = (f ·Q ))))
8180reximia 2408 . . . . . 6 (f (2ndA)f <Q xf (2ndA)(f <Q x (2nd ‘1P)x = (f ·Q )))
8241, 81syl 14 . . . . 5 ((A P x (2ndA)) → f (2ndA)(f <Q x (2nd ‘1P)x = (f ·Q )))
8382ex 108 . . . 4 (A P → (x (2ndA) → f (2ndA)(f <Q x (2nd ‘1P)x = (f ·Q ))))
84 prcunqu 6468 . . . . . . 7 ((⟨(1stA), (2ndA)⟩ P f (2ndA)) → (f <Q xx (2ndA)))
8510, 84sylan 267 . . . . . 6 ((A P f (2ndA)) → (f <Q xx (2ndA)))
8685adantrd 264 . . . . 5 ((A P f (2ndA)) → ((f <Q x (2nd ‘1P)x = (f ·Q )) → x (2ndA)))
8786rexlimdva 2427 . . . 4 (A P → (f (2ndA)(f <Q x (2nd ‘1P)x = (f ·Q )) → x (2ndA)))
8883, 87impbid 120 . . 3 (A P → (x (2ndA) ↔ f (2ndA)(f <Q x (2nd ‘1P)x = (f ·Q ))))
8935, 39, 883bitr4d 209 . 2 (A P → (x (2nd ‘(A ·P 1P)) ↔ x (2ndA)))
9089eqrdv 2035 1 (A P → (2nd ‘(A ·P 1P)) = (2ndA))
 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  1st c1st 5707  2nd c2nd 5708  Qcnq 6264  1Qc1q 6265   ·Q cmq 6267  *Qcrq 6268
 Copyright terms: Public domain W3C validator