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

Theorem 1idprl 6566
 Description: Lemma for 1idpr 6568. (Contributed by Jim Kingdon, 13-Dec-2019.)
Assertion
Ref Expression
1idprl (A P → (1st ‘(A ·P 1P)) = (1stA))

Proof of Theorem 1idprl
Dummy variables x y z w v u f g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 2958 . . . . . 6 (1st ‘1P) ⊆ (1st ‘1P)
2 rexss 3001 . . . . . 6 ((1st ‘1P) ⊆ (1st ‘1P) → (g (1st ‘1P)x = (f ·Q g) ↔ g (1st ‘1P)(g (1st ‘1P) x = (f ·Q g))))
31, 2ax-mp 7 . . . . 5 (g (1st ‘1P)x = (f ·Q g) ↔ g (1st ‘1P)(g (1st ‘1P) x = (f ·Q g)))
4 r19.42v 2461 . . . . . 6 (g (1st ‘1P)(x <Q f x = (f ·Q g)) ↔ (x <Q f g (1st ‘1P)x = (f ·Q g)))
5 1pr 6535 . . . . . . . . . . 11 1P P
6 prop 6458 . . . . . . . . . . . 12 (1P P → ⟨(1st ‘1P), (2nd ‘1P)⟩ P)
7 elprnql 6464 . . . . . . . . . . . 12 ((⟨(1st ‘1P), (2nd ‘1P)⟩ P g (1st ‘1P)) → g Q)
86, 7sylan 267 . . . . . . . . . . 11 ((1P P g (1st ‘1P)) → g Q)
95, 8mpan 400 . . . . . . . . . 10 (g (1st ‘1P) → g Q)
10 prop 6458 . . . . . . . . . . . 12 (A P → ⟨(1stA), (2ndA)⟩ P)
11 elprnql 6464 . . . . . . . . . . . 12 ((⟨(1stA), (2ndA)⟩ P f (1stA)) → f Q)
1210, 11sylan 267 . . . . . . . . . . 11 ((A P f (1stA)) → f Q)
13 breq1 3758 . . . . . . . . . . . . 13 (x = (f ·Q g) → (x <Q f ↔ (f ·Q g) <Q f))
14133ad2ant3 926 . . . . . . . . . . . 12 ((f Q g Q x = (f ·Q g)) → (x <Q f ↔ (f ·Q g) <Q f))
15 1prl 6536 . . . . . . . . . . . . . . 15 (1st ‘1P) = {gg <Q 1Q}
1615abeq2i 2145 . . . . . . . . . . . . . 14 (g (1st ‘1P) ↔ g <Q 1Q)
17 1nq 6350 . . . . . . . . . . . . . . . . 17 1Q Q
18 ltmnqg 6385 . . . . . . . . . . . . . . . . 17 ((g Q 1Q Q f Q) → (g <Q 1Q ↔ (f ·Q g) <Q (f ·Q 1Q)))
1917, 18mp3an2 1219 . . . . . . . . . . . . . . . 16 ((g Q f Q) → (g <Q 1Q ↔ (f ·Q g) <Q (f ·Q 1Q)))
2019ancoms 255 . . . . . . . . . . . . . . 15 ((f Q g Q) → (g <Q 1Q ↔ (f ·Q g) <Q (f ·Q 1Q)))
21 mulidnq 6373 . . . . . . . . . . . . . . . . 17 (f Q → (f ·Q 1Q) = f)
2221breq2d 3767 . . . . . . . . . . . . . . . 16 (f Q → ((f ·Q g) <Q (f ·Q 1Q) ↔ (f ·Q g) <Q f))
2322adantr 261 . . . . . . . . . . . . . . 15 ((f Q g Q) → ((f ·Q g) <Q (f ·Q 1Q) ↔ (f ·Q g) <Q f))
2420, 23bitrd 177 . . . . . . . . . . . . . 14 ((f Q g Q) → (g <Q 1Q ↔ (f ·Q g) <Q f))
2516, 24syl5rbb 182 . . . . . . . . . . . . 13 ((f Q g Q) → ((f ·Q g) <Q fg (1st ‘1P)))
26253adant3 923 . . . . . . . . . . . 12 ((f Q g Q x = (f ·Q g)) → ((f ·Q g) <Q fg (1st ‘1P)))
2714, 26bitrd 177 . . . . . . . . . . 11 ((f Q g Q x = (f ·Q g)) → (x <Q fg (1st ‘1P)))
2812, 27syl3an1 1167 . . . . . . . . . 10 (((A P f (1stA)) g Q x = (f ·Q g)) → (x <Q fg (1st ‘1P)))
299, 28syl3an2 1168 . . . . . . . . 9 (((A P f (1stA)) g (1st ‘1P) x = (f ·Q g)) → (x <Q fg (1st ‘1P)))
30293expia 1105 . . . . . . . 8 (((A P f (1stA)) g (1st ‘1P)) → (x = (f ·Q g) → (x <Q fg (1st ‘1P))))
3130pm5.32rd 424 . . . . . . 7 (((A P f (1stA)) g (1st ‘1P)) → ((x <Q f x = (f ·Q g)) ↔ (g (1st ‘1P) x = (f ·Q g))))
3231rexbidva 2317 . . . . . 6 ((A P f (1stA)) → (g (1st ‘1P)(x <Q f x = (f ·Q g)) ↔ g (1st ‘1P)(g (1st ‘1P) x = (f ·Q g))))
334, 32syl5rbbr 184 . . . . 5 ((A P f (1stA)) → (g (1st ‘1P)(g (1st ‘1P) x = (f ·Q g)) ↔ (x <Q f g (1st ‘1P)x = (f ·Q g))))
343, 33syl5bb 181 . . . 4 ((A P f (1stA)) → (g (1st ‘1P)x = (f ·Q g) ↔ (x <Q f g (1st ‘1P)x = (f ·Q g))))
3534rexbidva 2317 . . 3 (A P → (f (1stA)g (1st ‘1P)x = (f ·Q g) ↔ f (1stA)(x <Q f g (1st ‘1P)x = (f ·Q g))))
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, 37genpelvl 6495 . . . 4 ((A P 1P P) → (x (1st ‘(A ·P 1P)) ↔ f (1stA)g (1st ‘1P)x = (f ·Q g)))
395, 38mpan2 401 . . 3 (A P → (x (1st ‘(A ·P 1P)) ↔ f (1stA)g (1st ‘1P)x = (f ·Q g)))
40 prnmaxl 6471 . . . . . . 7 ((⟨(1stA), (2ndA)⟩ P x (1stA)) → f (1stA)x <Q f)
4110, 40sylan 267 . . . . . 6 ((A P x (1stA)) → f (1stA)x <Q f)
42 ltrelnq 6349 . . . . . . . . . . . . 13 <Q ⊆ (Q × Q)
4342brel 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)))
4544adantl 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 → (*Qf) Q)
4948adantl 262 . . . . . . . . . . . . . . 15 ((x Q f Q) → (*Qf) Q)
50 mulcomnqg 6367 . . . . . . . . . . . . . . . 16 ((y Q z Q) → (y ·Q z) = (z ·Q y))
5150adantl 262 . . . . . . . . . . . . . . 15 (((x Q f Q) (y Q z Q)) → (y ·Q z) = (z ·Q y))
5245, 46, 47, 49, 51caovord2d 5612 . . . . . . . . . . . . . 14 ((x Q f Q) → (x <Q f ↔ (x ·Q (*Qf)) <Q (f ·Q (*Qf))))
53 recidnq 6377 . . . . . . . . . . . . . . . 16 (f Q → (f ·Q (*Qf)) = 1Q)
5453breq2d 3767 . . . . . . . . . . . . . . 15 (f Q → ((x ·Q (*Qf)) <Q (f ·Q (*Qf)) ↔ (x ·Q (*Qf)) <Q 1Q))
5554adantl 262 . . . . . . . . . . . . . 14 ((x Q f Q) → ((x ·Q (*Qf)) <Q (f ·Q (*Qf)) ↔ (x ·Q (*Qf)) <Q 1Q))
5652, 55bitrd 177 . . . . . . . . . . . . 13 ((x Q f Q) → (x <Q f ↔ (x ·Q (*Qf)) <Q 1Q))
5756biimpd 132 . . . . . . . . . . . 12 ((x Q f Q) → (x <Q f → (x ·Q (*Qf)) <Q 1Q))
5843, 57mpcom 32 . . . . . . . . . . 11 (x <Q f → (x ·Q (*Qf)) <Q 1Q)
59 mulclnq 6360 . . . . . . . . . . . . . 14 ((x Q (*Qf) Q) → (x ·Q (*Qf)) Q)
6048, 59sylan2 270 . . . . . . . . . . . . 13 ((x Q f Q) → (x ·Q (*Qf)) Q)
6143, 60syl 14 . . . . . . . . . . . 12 (x <Q f → (x ·Q (*Qf)) Q)
62 breq1 3758 . . . . . . . . . . . . 13 (g = (x ·Q (*Qf)) → (g <Q 1Q ↔ (x ·Q (*Qf)) <Q 1Q))
6362, 15elab2g 2683 . . . . . . . . . . . 12 ((x ·Q (*Qf)) Q → ((x ·Q (*Qf)) (1st ‘1P) ↔ (x ·Q (*Qf)) <Q 1Q))
6461, 63syl 14 . . . . . . . . . . 11 (x <Q f → ((x ·Q (*Qf)) (1st ‘1P) ↔ (x ·Q (*Qf)) <Q 1Q))
6558, 64mpbird 156 . . . . . . . . . 10 (x <Q f → (x ·Q (*Qf)) (1st ‘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, 46, 49, 51, 67caov12d 5624 . . . . . . . . . . . 12 ((x Q f Q) → (f ·Q (x ·Q (*Qf))) = (x ·Q (f ·Q (*Qf))))
6953oveq2d 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))))
7443, 73syl 14 . . . . . . . . . 10 (x <Q fx = (f ·Q (x ·Q (*Qf))))
75 oveq2 5463 . . . . . . . . . . . 12 (g = (x ·Q (*Qf)) → (f ·Q g) = (f ·Q (x ·Q (*Qf))))
7675eqeq2d 2048 . . . . . . . . . . 11 (g = (x ·Q (*Qf)) → (x = (f ·Q g) ↔ x = (f ·Q (x ·Q (*Qf)))))
7776rspcev 2650 . . . . . . . . . 10 (((x ·Q (*Qf)) (1st ‘1P) x = (f ·Q (x ·Q (*Qf)))) → g (1st ‘1P)x = (f ·Q g))
7865, 74, 77syl2anc 391 . . . . . . . . 9 (x <Q fg (1st ‘1P)x = (f ·Q g))
7978a1i 9 . . . . . . . 8 (f (1stA) → (x <Q fg (1st ‘1P)x = (f ·Q g)))
8079ancld 308 . . . . . . 7 (f (1stA) → (x <Q f → (x <Q f g (1st ‘1P)x = (f ·Q g))))
8180reximia 2408 . . . . . 6 (f (1stA)x <Q ff (1stA)(x <Q f g (1st ‘1P)x = (f ·Q g)))
8241, 81syl 14 . . . . 5 ((A P x (1stA)) → f (1stA)(x <Q f g (1st ‘1P)x = (f ·Q g)))
8382ex 108 . . . 4 (A P → (x (1stA) → f (1stA)(x <Q f g (1st ‘1P)x = (f ·Q g))))
84 prcdnql 6467 . . . . . . 7 ((⟨(1stA), (2ndA)⟩ P f (1stA)) → (x <Q fx (1stA)))
8510, 84sylan 267 . . . . . 6 ((A P f (1stA)) → (x <Q fx (1stA)))
8685adantrd 264 . . . . 5 ((A P f (1stA)) → ((x <Q f g (1st ‘1P)x = (f ·Q g)) → x (1stA)))
8786rexlimdva 2427 . . . 4 (A P → (f (1stA)(x <Q f g (1st ‘1P)x = (f ·Q g)) → x (1stA)))
8883, 87impbid 120 . . 3 (A P → (x (1stA) ↔ f (1stA)(x <Q f g (1st ‘1P)x = (f ·Q g))))
8935, 39, 883bitr4d 209 . 2 (A P → (x (1st ‘(A ·P 1P)) ↔ x (1stA)))
9089eqrdv 2035 1 (A P → (1st ‘(A ·P 1P)) = (1stA))
 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