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

Theorem 1idpru 7581
Description: Lemma for 1idpr 7582. (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 3175 . . . . . 6 (2nd ‘1P) ⊆ (2nd ‘1P)
2 rexss 3222 . . . . . 6 ((2nd ‘1P) ⊆ (2nd ‘1P) → (∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ) ↔ ∃ ∈ (2nd ‘1P)( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q ))))
31, 2ax-mp 5 . . . . 5 (∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ) ↔ ∃ ∈ (2nd ‘1P)( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q )))
4 1pr 7544 . . . . . . . . . . 11 1PP
5 prop 7465 . . . . . . . . . . . 12 (1PP → ⟨(1st ‘1P), (2nd ‘1P)⟩ ∈ P)
6 elprnqu 7472 . . . . . . . . . . . 12 ((⟨(1st ‘1P), (2nd ‘1P)⟩ ∈ P ∈ (2nd ‘1P)) → Q)
75, 6sylan 283 . . . . . . . . . . 11 ((1PP ∈ (2nd ‘1P)) → Q)
84, 7mpan 424 . . . . . . . . . 10 ( ∈ (2nd ‘1P) → Q)
9 prop 7465 . . . . . . . . . . . 12 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
10 elprnqu 7472 . . . . . . . . . . . 12 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑓 ∈ (2nd𝐴)) → 𝑓Q)
119, 10sylan 283 . . . . . . . . . . 11 ((𝐴P𝑓 ∈ (2nd𝐴)) → 𝑓Q)
12 breq2 4004 . . . . . . . . . . . . 13 (𝑥 = (𝑓 ·Q ) → (𝑓 <Q 𝑥𝑓 <Q (𝑓 ·Q )))
13123ad2ant3 1020 . . . . . . . . . . . 12 ((𝑓QQ𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥𝑓 <Q (𝑓 ·Q )))
14 1pru 7546 . . . . . . . . . . . . . . 15 (2nd ‘1P) = { ∣ 1Q <Q }
1514abeq2i 2288 . . . . . . . . . . . . . 14 ( ∈ (2nd ‘1P) ↔ 1Q <Q )
16 1nq 7356 . . . . . . . . . . . . . . . . 17 1QQ
17 ltmnqg 7391 . . . . . . . . . . . . . . . . 17 ((1QQQ𝑓Q) → (1Q <Q ↔ (𝑓 ·Q 1Q) <Q (𝑓 ·Q )))
1816, 17mp3an1 1324 . . . . . . . . . . . . . . . 16 ((Q𝑓Q) → (1Q <Q ↔ (𝑓 ·Q 1Q) <Q (𝑓 ·Q )))
1918ancoms 268 . . . . . . . . . . . . . . 15 ((𝑓QQ) → (1Q <Q ↔ (𝑓 ·Q 1Q) <Q (𝑓 ·Q )))
20 mulidnq 7379 . . . . . . . . . . . . . . . . 17 (𝑓Q → (𝑓 ·Q 1Q) = 𝑓)
2120breq1d 4010 . . . . . . . . . . . . . . . 16 (𝑓Q → ((𝑓 ·Q 1Q) <Q (𝑓 ·Q ) ↔ 𝑓 <Q (𝑓 ·Q )))
2221adantr 276 . . . . . . . . . . . . . . 15 ((𝑓QQ) → ((𝑓 ·Q 1Q) <Q (𝑓 ·Q ) ↔ 𝑓 <Q (𝑓 ·Q )))
2319, 22bitrd 188 . . . . . . . . . . . . . 14 ((𝑓QQ) → (1Q <Q 𝑓 <Q (𝑓 ·Q )))
2415, 23bitr2id 193 . . . . . . . . . . . . 13 ((𝑓QQ) → (𝑓 <Q (𝑓 ·Q ) ↔ ∈ (2nd ‘1P)))
25243adant3 1017 . . . . . . . . . . . 12 ((𝑓QQ𝑥 = (𝑓 ·Q )) → (𝑓 <Q (𝑓 ·Q ) ↔ ∈ (2nd ‘1P)))
2613, 25bitrd 188 . . . . . . . . . . 11 ((𝑓QQ𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P)))
2711, 26syl3an1 1271 . . . . . . . . . 10 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ Q𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P)))
288, 27syl3an2 1272 . . . . . . . . 9 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P)))
29283expia 1205 . . . . . . . 8 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ ∈ (2nd ‘1P)) → (𝑥 = (𝑓 ·Q ) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P))))
3029pm5.32rd 451 . . . . . . 7 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ ∈ (2nd ‘1P)) → ((𝑓 <Q 𝑥𝑥 = (𝑓 ·Q )) ↔ ( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q ))))
3130rexbidva 2474 . . . . . 6 ((𝐴P𝑓 ∈ (2nd𝐴)) → (∃ ∈ (2nd ‘1P)(𝑓 <Q 𝑥𝑥 = (𝑓 ·Q )) ↔ ∃ ∈ (2nd ‘1P)( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q ))))
32 r19.42v 2634 . . . . . 6 (∃ ∈ (2nd ‘1P)(𝑓 <Q 𝑥𝑥 = (𝑓 ·Q )) ↔ (𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
3331, 32bitr3di 195 . . . . 5 ((𝐴P𝑓 ∈ (2nd𝐴)) → (∃ ∈ (2nd ‘1P)( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q )) ↔ (𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
343, 33bitrid 192 . . . 4 ((𝐴P𝑓 ∈ (2nd𝐴)) → (∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ) ↔ (𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
3534rexbidva 2474 . . 3 (𝐴P → (∃𝑓 ∈ (2nd𝐴)∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ) ↔ ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
36 df-imp 7459 . . . . 5 ·P = (𝑦P, 𝑧P ↦ ⟨{𝑤Q ∣ ∃𝑢Q𝑣Q (𝑢 ∈ (1st𝑦) ∧ 𝑣 ∈ (1st𝑧) ∧ 𝑤 = (𝑢 ·Q 𝑣))}, {𝑤Q ∣ ∃𝑢Q𝑣Q (𝑢 ∈ (2nd𝑦) ∧ 𝑣 ∈ (2nd𝑧) ∧ 𝑤 = (𝑢 ·Q 𝑣))}⟩)
37 mulclnq 7366 . . . . 5 ((𝑢Q𝑣Q) → (𝑢 ·Q 𝑣) ∈ Q)
3836, 37genpelvu 7503 . . . 4 ((𝐴P ∧ 1PP) → (𝑥 ∈ (2nd ‘(𝐴 ·P 1P)) ↔ ∃𝑓 ∈ (2nd𝐴)∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
394, 38mpan2 425 . . 3 (𝐴P → (𝑥 ∈ (2nd ‘(𝐴 ·P 1P)) ↔ ∃𝑓 ∈ (2nd𝐴)∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
40 prnminu 7479 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑥 ∈ (2nd𝐴)) → ∃𝑓 ∈ (2nd𝐴)𝑓 <Q 𝑥)
419, 40sylan 283 . . . . . 6 ((𝐴P𝑥 ∈ (2nd𝐴)) → ∃𝑓 ∈ (2nd𝐴)𝑓 <Q 𝑥)
42 ltrelnq 7355 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
4342brel 4675 . . . . . . . . . . . . 13 (𝑓 <Q 𝑥 → (𝑓Q𝑥Q))
4443ancomd 267 . . . . . . . . . . . 12 (𝑓 <Q 𝑥 → (𝑥Q𝑓Q))
45 ltmnqg 7391 . . . . . . . . . . . . . . . 16 ((𝑦Q𝑧Q𝑤Q) → (𝑦 <Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q (𝑤 ·Q 𝑧)))
4645adantl 277 . . . . . . . . . . . . . . 15 (((𝑥Q𝑓Q) ∧ (𝑦Q𝑧Q𝑤Q)) → (𝑦 <Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q (𝑤 ·Q 𝑧)))
47 simpr 110 . . . . . . . . . . . . . . 15 ((𝑥Q𝑓Q) → 𝑓Q)
48 simpl 109 . . . . . . . . . . . . . . 15 ((𝑥Q𝑓Q) → 𝑥Q)
49 recclnq 7382 . . . . . . . . . . . . . . . 16 (𝑓Q → (*Q𝑓) ∈ Q)
5049adantl 277 . . . . . . . . . . . . . . 15 ((𝑥Q𝑓Q) → (*Q𝑓) ∈ Q)
51 mulcomnqg 7373 . . . . . . . . . . . . . . . 16 ((𝑦Q𝑧Q) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦))
5251adantl 277 . . . . . . . . . . . . . . 15 (((𝑥Q𝑓Q) ∧ (𝑦Q𝑧Q)) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦))
5346, 47, 48, 50, 52caovord2d 6038 . . . . . . . . . . . . . 14 ((𝑥Q𝑓Q) → (𝑓 <Q 𝑥 ↔ (𝑓 ·Q (*Q𝑓)) <Q (𝑥 ·Q (*Q𝑓))))
54 recidnq 7383 . . . . . . . . . . . . . . . 16 (𝑓Q → (𝑓 ·Q (*Q𝑓)) = 1Q)
5554breq1d 4010 . . . . . . . . . . . . . . 15 (𝑓Q → ((𝑓 ·Q (*Q𝑓)) <Q (𝑥 ·Q (*Q𝑓)) ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
5655adantl 277 . . . . . . . . . . . . . 14 ((𝑥Q𝑓Q) → ((𝑓 ·Q (*Q𝑓)) <Q (𝑥 ·Q (*Q𝑓)) ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
5753, 56bitrd 188 . . . . . . . . . . . . 13 ((𝑥Q𝑓Q) → (𝑓 <Q 𝑥 ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
5857biimpd 144 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑓 <Q 𝑥 → 1Q <Q (𝑥 ·Q (*Q𝑓))))
5944, 58mpcom 36 . . . . . . . . . . 11 (𝑓 <Q 𝑥 → 1Q <Q (𝑥 ·Q (*Q𝑓)))
60 mulclnq 7366 . . . . . . . . . . . . 13 ((𝑥Q ∧ (*Q𝑓) ∈ Q) → (𝑥 ·Q (*Q𝑓)) ∈ Q)
6149, 60sylan2 286 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q (*Q𝑓)) ∈ Q)
62 breq2 4004 . . . . . . . . . . . . 13 ( = (𝑥 ·Q (*Q𝑓)) → (1Q <Q ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
6362, 14elab2g 2884 . . . . . . . . . . . 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 167 . . . . . . . . . 10 (𝑓 <Q 𝑥 → (𝑥 ·Q (*Q𝑓)) ∈ (2nd ‘1P))
66 mulassnqg 7374 . . . . . . . . . . . . . 14 ((𝑦Q𝑧Q𝑤Q) → ((𝑦 ·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧 ·Q 𝑤)))
6766adantl 277 . . . . . . . . . . . . 13 (((𝑥Q𝑓Q) ∧ (𝑦Q𝑧Q𝑤Q)) → ((𝑦 ·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧 ·Q 𝑤)))
6847, 48, 50, 52, 67caov12d 6050 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑓 ·Q (𝑥 ·Q (*Q𝑓))) = (𝑥 ·Q (𝑓 ·Q (*Q𝑓))))
6954oveq2d 5885 . . . . . . . . . . . . 13 (𝑓Q → (𝑥 ·Q (𝑓 ·Q (*Q𝑓))) = (𝑥 ·Q 1Q))
7069adantl 277 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q (𝑓 ·Q (*Q𝑓))) = (𝑥 ·Q 1Q))
71 mulidnq 7379 . . . . . . . . . . . . 13 (𝑥Q → (𝑥 ·Q 1Q) = 𝑥)
7271adantr 276 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q 1Q) = 𝑥)
7368, 70, 723eqtrrd 2215 . . . . . . . . . . 11 ((𝑥Q𝑓Q) → 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
7444, 73syl 14 . . . . . . . . . 10 (𝑓 <Q 𝑥𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
75 oveq2 5877 . . . . . . . . . . . 12 ( = (𝑥 ·Q (*Q𝑓)) → (𝑓 ·Q ) = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
7675eqeq2d 2189 . . . . . . . . . . 11 ( = (𝑥 ·Q (*Q𝑓)) → (𝑥 = (𝑓 ·Q ) ↔ 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓)))))
7776rspcev 2841 . . . . . . . . . 10 (((𝑥 ·Q (*Q𝑓)) ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓)))) → ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))
7865, 74, 77syl2anc 411 . . . . . . . . 9 (𝑓 <Q 𝑥 → ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))
7978a1i 9 . . . . . . . 8 (𝑓 ∈ (2nd𝐴) → (𝑓 <Q 𝑥 → ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
8079ancld 325 . . . . . . 7 (𝑓 ∈ (2nd𝐴) → (𝑓 <Q 𝑥 → (𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
8180reximia 2572 . . . . . 6 (∃𝑓 ∈ (2nd𝐴)𝑓 <Q 𝑥 → ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
8241, 81syl 14 . . . . 5 ((𝐴P𝑥 ∈ (2nd𝐴)) → ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
8382ex 115 . . . 4 (𝐴P → (𝑥 ∈ (2nd𝐴) → ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
84 prcunqu 7475 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑓 ∈ (2nd𝐴)) → (𝑓 <Q 𝑥𝑥 ∈ (2nd𝐴)))
859, 84sylan 283 . . . . . 6 ((𝐴P𝑓 ∈ (2nd𝐴)) → (𝑓 <Q 𝑥𝑥 ∈ (2nd𝐴)))
8685adantrd 279 . . . . 5 ((𝐴P𝑓 ∈ (2nd𝐴)) → ((𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )) → 𝑥 ∈ (2nd𝐴)))
8786rexlimdva 2594 . . . 4 (𝐴P → (∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )) → 𝑥 ∈ (2nd𝐴)))
8883, 87impbid 129 . . 3 (𝐴P → (𝑥 ∈ (2nd𝐴) ↔ ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
8935, 39, 883bitr4d 220 . 2 (𝐴P → (𝑥 ∈ (2nd ‘(𝐴 ·P 1P)) ↔ 𝑥 ∈ (2nd𝐴)))
9089eqrdv 2175 1 (𝐴P → (2nd ‘(𝐴 ·P 1P)) = (2nd𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978   = wceq 1353  wcel 2148  wrex 2456  wss 3129  cop 3594   class class class wbr 4000  cfv 5212  (class class class)co 5869  1st c1st 6133  2nd c2nd 6134  Qcnq 7270  1Qc1q 7271   ·Q cmq 7273  *Qcrq 7274   <Q cltq 7275  Pcnp 7281  1Pc1p 7282   ·P cmp 7284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-eprel 4286  df-id 4290  df-po 4293  df-iso 4294  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-irdg 6365  df-1o 6411  df-oadd 6415  df-omul 6416  df-er 6529  df-ec 6531  df-qs 6535  df-ni 7294  df-pli 7295  df-mi 7296  df-lti 7297  df-plpq 7334  df-mpq 7335  df-enq 7337  df-nqqs 7338  df-plqqs 7339  df-mqqs 7340  df-1nqqs 7341  df-rq 7342  df-ltnqqs 7343  df-inp 7456  df-i1p 7457  df-imp 7459
This theorem is referenced by:  1idpr  7582
  Copyright terms: Public domain W3C validator