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

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

Proof of Theorem 1idpru
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 2964 . . . . . 6 (2nd ‘1P) ⊆ (2nd ‘1P)
2 rexss 3007 . . . . . 6 ((2nd ‘1P) ⊆ (2nd ‘1P) → (∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ) ↔ ∃ ∈ (2nd ‘1P)( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q ))))
31, 2ax-mp 7 . . . . 5 (∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ) ↔ ∃ ∈ (2nd ‘1P)( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q )))
4 r19.42v 2467 . . . . . 6 (∃ ∈ (2nd ‘1P)(𝑓 <Q 𝑥𝑥 = (𝑓 ·Q )) ↔ (𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
5 1pr 6652 . . . . . . . . . . 11 1PP
6 prop 6573 . . . . . . . . . . . 12 (1PP → ⟨(1st ‘1P), (2nd ‘1P)⟩ ∈ P)
7 elprnqu 6580 . . . . . . . . . . . 12 ((⟨(1st ‘1P), (2nd ‘1P)⟩ ∈ P ∈ (2nd ‘1P)) → Q)
86, 7sylan 267 . . . . . . . . . . 11 ((1PP ∈ (2nd ‘1P)) → Q)
95, 8mpan 400 . . . . . . . . . 10 ( ∈ (2nd ‘1P) → Q)
10 prop 6573 . . . . . . . . . . . 12 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
11 elprnqu 6580 . . . . . . . . . . . 12 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑓 ∈ (2nd𝐴)) → 𝑓Q)
1210, 11sylan 267 . . . . . . . . . . 11 ((𝐴P𝑓 ∈ (2nd𝐴)) → 𝑓Q)
13 breq2 3768 . . . . . . . . . . . . 13 (𝑥 = (𝑓 ·Q ) → (𝑓 <Q 𝑥𝑓 <Q (𝑓 ·Q )))
14133ad2ant3 927 . . . . . . . . . . . 12 ((𝑓QQ𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥𝑓 <Q (𝑓 ·Q )))
15 1pru 6654 . . . . . . . . . . . . . . 15 (2nd ‘1P) = { ∣ 1Q <Q }
1615abeq2i 2148 . . . . . . . . . . . . . 14 ( ∈ (2nd ‘1P) ↔ 1Q <Q )
17 1nq 6464 . . . . . . . . . . . . . . . . 17 1QQ
18 ltmnqg 6499 . . . . . . . . . . . . . . . . 17 ((1QQQ𝑓Q) → (1Q <Q ↔ (𝑓 ·Q 1Q) <Q (𝑓 ·Q )))
1917, 18mp3an1 1219 . . . . . . . . . . . . . . . 16 ((Q𝑓Q) → (1Q <Q ↔ (𝑓 ·Q 1Q) <Q (𝑓 ·Q )))
2019ancoms 255 . . . . . . . . . . . . . . 15 ((𝑓QQ) → (1Q <Q ↔ (𝑓 ·Q 1Q) <Q (𝑓 ·Q )))
21 mulidnq 6487 . . . . . . . . . . . . . . . . 17 (𝑓Q → (𝑓 ·Q 1Q) = 𝑓)
2221breq1d 3774 . . . . . . . . . . . . . . . 16 (𝑓Q → ((𝑓 ·Q 1Q) <Q (𝑓 ·Q ) ↔ 𝑓 <Q (𝑓 ·Q )))
2322adantr 261 . . . . . . . . . . . . . . 15 ((𝑓QQ) → ((𝑓 ·Q 1Q) <Q (𝑓 ·Q ) ↔ 𝑓 <Q (𝑓 ·Q )))
2420, 23bitrd 177 . . . . . . . . . . . . . 14 ((𝑓QQ) → (1Q <Q 𝑓 <Q (𝑓 ·Q )))
2516, 24syl5rbb 182 . . . . . . . . . . . . 13 ((𝑓QQ) → (𝑓 <Q (𝑓 ·Q ) ↔ ∈ (2nd ‘1P)))
26253adant3 924 . . . . . . . . . . . 12 ((𝑓QQ𝑥 = (𝑓 ·Q )) → (𝑓 <Q (𝑓 ·Q ) ↔ ∈ (2nd ‘1P)))
2714, 26bitrd 177 . . . . . . . . . . 11 ((𝑓QQ𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P)))
2812, 27syl3an1 1168 . . . . . . . . . 10 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ Q𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P)))
299, 28syl3an2 1169 . . . . . . . . 9 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P)))
30293expia 1106 . . . . . . . 8 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ ∈ (2nd ‘1P)) → (𝑥 = (𝑓 ·Q ) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P))))
3130pm5.32rd 424 . . . . . . 7 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ ∈ (2nd ‘1P)) → ((𝑓 <Q 𝑥𝑥 = (𝑓 ·Q )) ↔ ( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q ))))
3231rexbidva 2323 . . . . . 6 ((𝐴P𝑓 ∈ (2nd𝐴)) → (∃ ∈ (2nd ‘1P)(𝑓 <Q 𝑥𝑥 = (𝑓 ·Q )) ↔ ∃ ∈ (2nd ‘1P)( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q ))))
334, 32syl5rbbr 184 . . . . 5 ((𝐴P𝑓 ∈ (2nd𝐴)) → (∃ ∈ (2nd ‘1P)( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q )) ↔ (𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
343, 33syl5bb 181 . . . 4 ((𝐴P𝑓 ∈ (2nd𝐴)) → (∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ) ↔ (𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
3534rexbidva 2323 . . 3 (𝐴P → (∃𝑓 ∈ (2nd𝐴)∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ) ↔ ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
36 df-imp 6567 . . . . 5 ·P = (𝑦P, 𝑧P ↦ ⟨{𝑤Q ∣ ∃𝑢Q𝑣Q (𝑢 ∈ (1st𝑦) ∧ 𝑣 ∈ (1st𝑧) ∧ 𝑤 = (𝑢 ·Q 𝑣))}, {𝑤Q ∣ ∃𝑢Q𝑣Q (𝑢 ∈ (2nd𝑦) ∧ 𝑣 ∈ (2nd𝑧) ∧ 𝑤 = (𝑢 ·Q 𝑣))}⟩)
37 mulclnq 6474 . . . . 5 ((𝑢Q𝑣Q) → (𝑢 ·Q 𝑣) ∈ Q)
3836, 37genpelvu 6611 . . . 4 ((𝐴P ∧ 1PP) → (𝑥 ∈ (2nd ‘(𝐴 ·P 1P)) ↔ ∃𝑓 ∈ (2nd𝐴)∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
395, 38mpan2 401 . . 3 (𝐴P → (𝑥 ∈ (2nd ‘(𝐴 ·P 1P)) ↔ ∃𝑓 ∈ (2nd𝐴)∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
40 prnminu 6587 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑥 ∈ (2nd𝐴)) → ∃𝑓 ∈ (2nd𝐴)𝑓 <Q 𝑥)
4110, 40sylan 267 . . . . . 6 ((𝐴P𝑥 ∈ (2nd𝐴)) → ∃𝑓 ∈ (2nd𝐴)𝑓 <Q 𝑥)
42 ltrelnq 6463 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
4342brel 4392 . . . . . . . . . . . . 13 (𝑓 <Q 𝑥 → (𝑓Q𝑥Q))
4443ancomd 254 . . . . . . . . . . . 12 (𝑓 <Q 𝑥 → (𝑥Q𝑓Q))
45 ltmnqg 6499 . . . . . . . . . . . . . . . 16 ((𝑦Q𝑧Q𝑤Q) → (𝑦 <Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q (𝑤 ·Q 𝑧)))
4645adantl 262 . . . . . . . . . . . . . . 15 (((𝑥Q𝑓Q) ∧ (𝑦Q𝑧Q𝑤Q)) → (𝑦 <Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q (𝑤 ·Q 𝑧)))
47 simpr 103 . . . . . . . . . . . . . . 15 ((𝑥Q𝑓Q) → 𝑓Q)
48 simpl 102 . . . . . . . . . . . . . . 15 ((𝑥Q𝑓Q) → 𝑥Q)
49 recclnq 6490 . . . . . . . . . . . . . . . 16 (𝑓Q → (*Q𝑓) ∈ Q)
5049adantl 262 . . . . . . . . . . . . . . 15 ((𝑥Q𝑓Q) → (*Q𝑓) ∈ Q)
51 mulcomnqg 6481 . . . . . . . . . . . . . . . 16 ((𝑦Q𝑧Q) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦))
5251adantl 262 . . . . . . . . . . . . . . 15 (((𝑥Q𝑓Q) ∧ (𝑦Q𝑧Q)) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦))
5346, 47, 48, 50, 52caovord2d 5670 . . . . . . . . . . . . . 14 ((𝑥Q𝑓Q) → (𝑓 <Q 𝑥 ↔ (𝑓 ·Q (*Q𝑓)) <Q (𝑥 ·Q (*Q𝑓))))
54 recidnq 6491 . . . . . . . . . . . . . . . 16 (𝑓Q → (𝑓 ·Q (*Q𝑓)) = 1Q)
5554breq1d 3774 . . . . . . . . . . . . . . 15 (𝑓Q → ((𝑓 ·Q (*Q𝑓)) <Q (𝑥 ·Q (*Q𝑓)) ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
5655adantl 262 . . . . . . . . . . . . . 14 ((𝑥Q𝑓Q) → ((𝑓 ·Q (*Q𝑓)) <Q (𝑥 ·Q (*Q𝑓)) ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
5753, 56bitrd 177 . . . . . . . . . . . . 13 ((𝑥Q𝑓Q) → (𝑓 <Q 𝑥 ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
5857biimpd 132 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑓 <Q 𝑥 → 1Q <Q (𝑥 ·Q (*Q𝑓))))
5944, 58mpcom 32 . . . . . . . . . . 11 (𝑓 <Q 𝑥 → 1Q <Q (𝑥 ·Q (*Q𝑓)))
60 mulclnq 6474 . . . . . . . . . . . . 13 ((𝑥Q ∧ (*Q𝑓) ∈ Q) → (𝑥 ·Q (*Q𝑓)) ∈ Q)
6149, 60sylan2 270 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q (*Q𝑓)) ∈ Q)
62 breq2 3768 . . . . . . . . . . . . 13 ( = (𝑥 ·Q (*Q𝑓)) → (1Q <Q ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
6362, 15elab2g 2689 . . . . . . . . . . . 12 ((𝑥 ·Q (*Q𝑓)) ∈ Q → ((𝑥 ·Q (*Q𝑓)) ∈ (2nd ‘1P) ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
6444, 61, 633syl 17 . . . . . . . . . . 11 (𝑓 <Q 𝑥 → ((𝑥 ·Q (*Q𝑓)) ∈ (2nd ‘1P) ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
6559, 64mpbird 156 . . . . . . . . . 10 (𝑓 <Q 𝑥 → (𝑥 ·Q (*Q𝑓)) ∈ (2nd ‘1P))
66 mulassnqg 6482 . . . . . . . . . . . . . 14 ((𝑦Q𝑧Q𝑤Q) → ((𝑦 ·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧 ·Q 𝑤)))
6766adantl 262 . . . . . . . . . . . . 13 (((𝑥Q𝑓Q) ∧ (𝑦Q𝑧Q𝑤Q)) → ((𝑦 ·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧 ·Q 𝑤)))
6847, 48, 50, 52, 67caov12d 5682 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑓 ·Q (𝑥 ·Q (*Q𝑓))) = (𝑥 ·Q (𝑓 ·Q (*Q𝑓))))
6954oveq2d 5528 . . . . . . . . . . . . 13 (𝑓Q → (𝑥 ·Q (𝑓 ·Q (*Q𝑓))) = (𝑥 ·Q 1Q))
7069adantl 262 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q (𝑓 ·Q (*Q𝑓))) = (𝑥 ·Q 1Q))
71 mulidnq 6487 . . . . . . . . . . . . 13 (𝑥Q → (𝑥 ·Q 1Q) = 𝑥)
7271adantr 261 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q 1Q) = 𝑥)
7368, 70, 723eqtrrd 2077 . . . . . . . . . . 11 ((𝑥Q𝑓Q) → 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
7444, 73syl 14 . . . . . . . . . 10 (𝑓 <Q 𝑥𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
75 oveq2 5520 . . . . . . . . . . . 12 ( = (𝑥 ·Q (*Q𝑓)) → (𝑓 ·Q ) = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
7675eqeq2d 2051 . . . . . . . . . . 11 ( = (𝑥 ·Q (*Q𝑓)) → (𝑥 = (𝑓 ·Q ) ↔ 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓)))))
7776rspcev 2656 . . . . . . . . . 10 (((𝑥 ·Q (*Q𝑓)) ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓)))) → ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))
7865, 74, 77syl2anc 391 . . . . . . . . 9 (𝑓 <Q 𝑥 → ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))
7978a1i 9 . . . . . . . 8 (𝑓 ∈ (2nd𝐴) → (𝑓 <Q 𝑥 → ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
8079ancld 308 . . . . . . 7 (𝑓 ∈ (2nd𝐴) → (𝑓 <Q 𝑥 → (𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
8180reximia 2414 . . . . . 6 (∃𝑓 ∈ (2nd𝐴)𝑓 <Q 𝑥 → ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
8241, 81syl 14 . . . . 5 ((𝐴P𝑥 ∈ (2nd𝐴)) → ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
8382ex 108 . . . 4 (𝐴P → (𝑥 ∈ (2nd𝐴) → ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
84 prcunqu 6583 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑓 ∈ (2nd𝐴)) → (𝑓 <Q 𝑥𝑥 ∈ (2nd𝐴)))
8510, 84sylan 267 . . . . . 6 ((𝐴P𝑓 ∈ (2nd𝐴)) → (𝑓 <Q 𝑥𝑥 ∈ (2nd𝐴)))
8685adantrd 264 . . . . 5 ((𝐴P𝑓 ∈ (2nd𝐴)) → ((𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )) → 𝑥 ∈ (2nd𝐴)))
8786rexlimdva 2433 . . . 4 (𝐴P → (∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )) → 𝑥 ∈ (2nd𝐴)))
8883, 87impbid 120 . . 3 (𝐴P → (𝑥 ∈ (2nd𝐴) ↔ ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
8935, 39, 883bitr4d 209 . 2 (𝐴P → (𝑥 ∈ (2nd ‘(𝐴 ·P 1P)) ↔ 𝑥 ∈ (2nd𝐴)))
9089eqrdv 2038 1 (𝐴P → (2nd ‘(𝐴 ·P 1P)) = (2nd𝐴))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 885   = wceq 1243   ∈ wcel 1393  ∃wrex 2307   ⊆ wss 2917  ⟨cop 3378   class class class wbr 3764  ‘cfv 4902  (class class class)co 5512  1st c1st 5765  2nd c2nd 5766  Qcnq 6378  1Qc1q 6379   ·Q cmq 6381  *Qcrq 6382
 Copyright terms: Public domain W3C validator