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

Theorem 1idpru 7615
Description: Lemma for 1idpr 7616. (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 3190 . . . . . 6 (2nd ‘1P) ⊆ (2nd ‘1P)
2 rexss 3237 . . . . . 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 7578 . . . . . . . . . . 11 1PP
5 prop 7499 . . . . . . . . . . . 12 (1PP → ⟨(1st ‘1P), (2nd ‘1P)⟩ ∈ P)
6 elprnqu 7506 . . . . . . . . . . . 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 7499 . . . . . . . . . . . 12 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
10 elprnqu 7506 . . . . . . . . . . . 12 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑓 ∈ (2nd𝐴)) → 𝑓Q)
119, 10sylan 283 . . . . . . . . . . 11 ((𝐴P𝑓 ∈ (2nd𝐴)) → 𝑓Q)
12 breq2 4022 . . . . . . . . . . . . 13 (𝑥 = (𝑓 ·Q ) → (𝑓 <Q 𝑥𝑓 <Q (𝑓 ·Q )))
13123ad2ant3 1022 . . . . . . . . . . . 12 ((𝑓QQ𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥𝑓 <Q (𝑓 ·Q )))
14 1pru 7580 . . . . . . . . . . . . . . 15 (2nd ‘1P) = { ∣ 1Q <Q }
1514abeq2i 2300 . . . . . . . . . . . . . 14 ( ∈ (2nd ‘1P) ↔ 1Q <Q )
16 1nq 7390 . . . . . . . . . . . . . . . . 17 1QQ
17 ltmnqg 7425 . . . . . . . . . . . . . . . . 17 ((1QQQ𝑓Q) → (1Q <Q ↔ (𝑓 ·Q 1Q) <Q (𝑓 ·Q )))
1816, 17mp3an1 1335 . . . . . . . . . . . . . . . 16 ((Q𝑓Q) → (1Q <Q ↔ (𝑓 ·Q 1Q) <Q (𝑓 ·Q )))
1918ancoms 268 . . . . . . . . . . . . . . 15 ((𝑓QQ) → (1Q <Q ↔ (𝑓 ·Q 1Q) <Q (𝑓 ·Q )))
20 mulidnq 7413 . . . . . . . . . . . . . . . . 17 (𝑓Q → (𝑓 ·Q 1Q) = 𝑓)
2120breq1d 4028 . . . . . . . . . . . . . . . 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 1019 . . . . . . . . . . . 12 ((𝑓QQ𝑥 = (𝑓 ·Q )) → (𝑓 <Q (𝑓 ·Q ) ↔ ∈ (2nd ‘1P)))
2613, 25bitrd 188 . . . . . . . . . . 11 ((𝑓QQ𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P)))
2711, 26syl3an1 1282 . . . . . . . . . 10 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ Q𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P)))
288, 27syl3an2 1283 . . . . . . . . 9 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q )) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P)))
29283expia 1207 . . . . . . . 8 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ ∈ (2nd ‘1P)) → (𝑥 = (𝑓 ·Q ) → (𝑓 <Q 𝑥 ∈ (2nd ‘1P))))
3029pm5.32rd 451 . . . . . . 7 (((𝐴P𝑓 ∈ (2nd𝐴)) ∧ ∈ (2nd ‘1P)) → ((𝑓 <Q 𝑥𝑥 = (𝑓 ·Q )) ↔ ( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q ))))
3130rexbidva 2487 . . . . . 6 ((𝐴P𝑓 ∈ (2nd𝐴)) → (∃ ∈ (2nd ‘1P)(𝑓 <Q 𝑥𝑥 = (𝑓 ·Q )) ↔ ∃ ∈ (2nd ‘1P)( ∈ (2nd ‘1P) ∧ 𝑥 = (𝑓 ·Q ))))
32 r19.42v 2647 . . . . . 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 2487 . . 3 (𝐴P → (∃𝑓 ∈ (2nd𝐴)∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ) ↔ ∃𝑓 ∈ (2nd𝐴)(𝑓 <Q 𝑥 ∧ ∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q ))))
36 df-imp 7493 . . . . 5 ·P = (𝑦P, 𝑧P ↦ ⟨{𝑤Q ∣ ∃𝑢Q𝑣Q (𝑢 ∈ (1st𝑦) ∧ 𝑣 ∈ (1st𝑧) ∧ 𝑤 = (𝑢 ·Q 𝑣))}, {𝑤Q ∣ ∃𝑢Q𝑣Q (𝑢 ∈ (2nd𝑦) ∧ 𝑣 ∈ (2nd𝑧) ∧ 𝑤 = (𝑢 ·Q 𝑣))}⟩)
37 mulclnq 7400 . . . . 5 ((𝑢Q𝑣Q) → (𝑢 ·Q 𝑣) ∈ Q)
3836, 37genpelvu 7537 . . . 4 ((𝐴P ∧ 1PP) → (𝑥 ∈ (2nd ‘(𝐴 ·P 1P)) ↔ ∃𝑓 ∈ (2nd𝐴)∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
394, 38mpan2 425 . . 3 (𝐴P → (𝑥 ∈ (2nd ‘(𝐴 ·P 1P)) ↔ ∃𝑓 ∈ (2nd𝐴)∃ ∈ (2nd ‘1P)𝑥 = (𝑓 ·Q )))
40 prnminu 7513 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑥 ∈ (2nd𝐴)) → ∃𝑓 ∈ (2nd𝐴)𝑓 <Q 𝑥)
419, 40sylan 283 . . . . . 6 ((𝐴P𝑥 ∈ (2nd𝐴)) → ∃𝑓 ∈ (2nd𝐴)𝑓 <Q 𝑥)
42 ltrelnq 7389 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
4342brel 4693 . . . . . . . . . . . . 13 (𝑓 <Q 𝑥 → (𝑓Q𝑥Q))
4443ancomd 267 . . . . . . . . . . . 12 (𝑓 <Q 𝑥 → (𝑥Q𝑓Q))
45 ltmnqg 7425 . . . . . . . . . . . . . . . 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 7416 . . . . . . . . . . . . . . . 16 (𝑓Q → (*Q𝑓) ∈ Q)
5049adantl 277 . . . . . . . . . . . . . . 15 ((𝑥Q𝑓Q) → (*Q𝑓) ∈ Q)
51 mulcomnqg 7407 . . . . . . . . . . . . . . . 16 ((𝑦Q𝑧Q) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦))
5251adantl 277 . . . . . . . . . . . . . . 15 (((𝑥Q𝑓Q) ∧ (𝑦Q𝑧Q)) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦))
5346, 47, 48, 50, 52caovord2d 6062 . . . . . . . . . . . . . 14 ((𝑥Q𝑓Q) → (𝑓 <Q 𝑥 ↔ (𝑓 ·Q (*Q𝑓)) <Q (𝑥 ·Q (*Q𝑓))))
54 recidnq 7417 . . . . . . . . . . . . . . . 16 (𝑓Q → (𝑓 ·Q (*Q𝑓)) = 1Q)
5554breq1d 4028 . . . . . . . . . . . . . . 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 7400 . . . . . . . . . . . . 13 ((𝑥Q ∧ (*Q𝑓) ∈ Q) → (𝑥 ·Q (*Q𝑓)) ∈ Q)
6149, 60sylan2 286 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q (*Q𝑓)) ∈ Q)
62 breq2 4022 . . . . . . . . . . . . 13 ( = (𝑥 ·Q (*Q𝑓)) → (1Q <Q ↔ 1Q <Q (𝑥 ·Q (*Q𝑓))))
6362, 14elab2g 2899 . . . . . . . . . . . 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 7408 . . . . . . . . . . . . . 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 6074 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑓 ·Q (𝑥 ·Q (*Q𝑓))) = (𝑥 ·Q (𝑓 ·Q (*Q𝑓))))
6954oveq2d 5908 . . . . . . . . . . . . 13 (𝑓Q → (𝑥 ·Q (𝑓 ·Q (*Q𝑓))) = (𝑥 ·Q 1Q))
7069adantl 277 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q (𝑓 ·Q (*Q𝑓))) = (𝑥 ·Q 1Q))
71 mulidnq 7413 . . . . . . . . . . . . 13 (𝑥Q → (𝑥 ·Q 1Q) = 𝑥)
7271adantr 276 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q 1Q) = 𝑥)
7368, 70, 723eqtrrd 2227 . . . . . . . . . . 11 ((𝑥Q𝑓Q) → 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
7444, 73syl 14 . . . . . . . . . 10 (𝑓 <Q 𝑥𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
75 oveq2 5900 . . . . . . . . . . . 12 ( = (𝑥 ·Q (*Q𝑓)) → (𝑓 ·Q ) = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
7675eqeq2d 2201 . . . . . . . . . . 11 ( = (𝑥 ·Q (*Q𝑓)) → (𝑥 = (𝑓 ·Q ) ↔ 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓)))))
7776rspcev 2856 . . . . . . . . . 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 2585 . . . . . 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 7509 . . . . . . 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 2607 . . . 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 2187 1 (𝐴P → (2nd ‘(𝐴 ·P 1P)) = (2nd𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 980   = wceq 1364  wcel 2160  wrex 2469  wss 3144  cop 3610   class class class wbr 4018  cfv 5232  (class class class)co 5892  1st c1st 6158  2nd c2nd 6159  Qcnq 7304  1Qc1q 7305   ·Q cmq 7307  *Qcrq 7308   <Q cltq 7309  Pcnp 7315  1Pc1p 7316   ·P cmp 7318
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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-eprel 4304  df-id 4308  df-po 4311  df-iso 4312  df-iord 4381  df-on 4383  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5234  df-fn 5235  df-f 5236  df-f1 5237  df-fo 5238  df-f1o 5239  df-fv 5240  df-ov 5895  df-oprab 5896  df-mpo 5897  df-1st 6160  df-2nd 6161  df-recs 6325  df-irdg 6390  df-1o 6436  df-oadd 6440  df-omul 6441  df-er 6554  df-ec 6556  df-qs 6560  df-ni 7328  df-pli 7329  df-mi 7330  df-lti 7331  df-plpq 7368  df-mpq 7369  df-enq 7371  df-nqqs 7372  df-plqqs 7373  df-mqqs 7374  df-1nqqs 7375  df-rq 7376  df-ltnqqs 7377  df-inp 7490  df-i1p 7491  df-imp 7493
This theorem is referenced by:  1idpr  7616
  Copyright terms: Public domain W3C validator