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

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

Proof of Theorem 1idprl
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 2992 . . . . . 6 (1st ‘1P) ⊆ (1st ‘1P)
2 rexss 3035 . . . . . 6 ((1st ‘1P) ⊆ (1st ‘1P) → (∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔) ↔ ∃𝑔 ∈ (1st ‘1P)(𝑔 ∈ (1st ‘1P) ∧ 𝑥 = (𝑓 ·Q 𝑔))))
31, 2ax-mp 7 . . . . 5 (∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔) ↔ ∃𝑔 ∈ (1st ‘1P)(𝑔 ∈ (1st ‘1P) ∧ 𝑥 = (𝑓 ·Q 𝑔)))
4 r19.42v 2484 . . . . . 6 (∃𝑔 ∈ (1st ‘1P)(𝑥 <Q 𝑓𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔)))
5 1pr 6710 . . . . . . . . . . 11 1PP
6 prop 6631 . . . . . . . . . . . 12 (1PP → ⟨(1st ‘1P), (2nd ‘1P)⟩ ∈ P)
7 elprnql 6637 . . . . . . . . . . . 12 ((⟨(1st ‘1P), (2nd ‘1P)⟩ ∈ P𝑔 ∈ (1st ‘1P)) → 𝑔Q)
86, 7sylan 271 . . . . . . . . . . 11 ((1PP𝑔 ∈ (1st ‘1P)) → 𝑔Q)
95, 8mpan 408 . . . . . . . . . 10 (𝑔 ∈ (1st ‘1P) → 𝑔Q)
10 prop 6631 . . . . . . . . . . . 12 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
11 elprnql 6637 . . . . . . . . . . . 12 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑓 ∈ (1st𝐴)) → 𝑓Q)
1210, 11sylan 271 . . . . . . . . . . 11 ((𝐴P𝑓 ∈ (1st𝐴)) → 𝑓Q)
13 breq1 3795 . . . . . . . . . . . . 13 (𝑥 = (𝑓 ·Q 𝑔) → (𝑥 <Q 𝑓 ↔ (𝑓 ·Q 𝑔) <Q 𝑓))
14133ad2ant3 938 . . . . . . . . . . . 12 ((𝑓Q𝑔Q𝑥 = (𝑓 ·Q 𝑔)) → (𝑥 <Q 𝑓 ↔ (𝑓 ·Q 𝑔) <Q 𝑓))
15 1prl 6711 . . . . . . . . . . . . . . 15 (1st ‘1P) = {𝑔𝑔 <Q 1Q}
1615abeq2i 2164 . . . . . . . . . . . . . 14 (𝑔 ∈ (1st ‘1P) ↔ 𝑔 <Q 1Q)
17 1nq 6522 . . . . . . . . . . . . . . . . 17 1QQ
18 ltmnqg 6557 . . . . . . . . . . . . . . . . 17 ((𝑔Q ∧ 1QQ𝑓Q) → (𝑔 <Q 1Q ↔ (𝑓 ·Q 𝑔) <Q (𝑓 ·Q 1Q)))
1917, 18mp3an2 1231 . . . . . . . . . . . . . . . 16 ((𝑔Q𝑓Q) → (𝑔 <Q 1Q ↔ (𝑓 ·Q 𝑔) <Q (𝑓 ·Q 1Q)))
2019ancoms 259 . . . . . . . . . . . . . . 15 ((𝑓Q𝑔Q) → (𝑔 <Q 1Q ↔ (𝑓 ·Q 𝑔) <Q (𝑓 ·Q 1Q)))
21 mulidnq 6545 . . . . . . . . . . . . . . . . 17 (𝑓Q → (𝑓 ·Q 1Q) = 𝑓)
2221breq2d 3804 . . . . . . . . . . . . . . . 16 (𝑓Q → ((𝑓 ·Q 𝑔) <Q (𝑓 ·Q 1Q) ↔ (𝑓 ·Q 𝑔) <Q 𝑓))
2322adantr 265 . . . . . . . . . . . . . . 15 ((𝑓Q𝑔Q) → ((𝑓 ·Q 𝑔) <Q (𝑓 ·Q 1Q) ↔ (𝑓 ·Q 𝑔) <Q 𝑓))
2420, 23bitrd 181 . . . . . . . . . . . . . 14 ((𝑓Q𝑔Q) → (𝑔 <Q 1Q ↔ (𝑓 ·Q 𝑔) <Q 𝑓))
2516, 24syl5rbb 186 . . . . . . . . . . . . 13 ((𝑓Q𝑔Q) → ((𝑓 ·Q 𝑔) <Q 𝑓𝑔 ∈ (1st ‘1P)))
26253adant3 935 . . . . . . . . . . . 12 ((𝑓Q𝑔Q𝑥 = (𝑓 ·Q 𝑔)) → ((𝑓 ·Q 𝑔) <Q 𝑓𝑔 ∈ (1st ‘1P)))
2714, 26bitrd 181 . . . . . . . . . . 11 ((𝑓Q𝑔Q𝑥 = (𝑓 ·Q 𝑔)) → (𝑥 <Q 𝑓𝑔 ∈ (1st ‘1P)))
2812, 27syl3an1 1179 . . . . . . . . . 10 (((𝐴P𝑓 ∈ (1st𝐴)) ∧ 𝑔Q𝑥 = (𝑓 ·Q 𝑔)) → (𝑥 <Q 𝑓𝑔 ∈ (1st ‘1P)))
299, 28syl3an2 1180 . . . . . . . . 9 (((𝐴P𝑓 ∈ (1st𝐴)) ∧ 𝑔 ∈ (1st ‘1P) ∧ 𝑥 = (𝑓 ·Q 𝑔)) → (𝑥 <Q 𝑓𝑔 ∈ (1st ‘1P)))
30293expia 1117 . . . . . . . 8 (((𝐴P𝑓 ∈ (1st𝐴)) ∧ 𝑔 ∈ (1st ‘1P)) → (𝑥 = (𝑓 ·Q 𝑔) → (𝑥 <Q 𝑓𝑔 ∈ (1st ‘1P))))
3130pm5.32rd 432 . . . . . . 7 (((𝐴P𝑓 ∈ (1st𝐴)) ∧ 𝑔 ∈ (1st ‘1P)) → ((𝑥 <Q 𝑓𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑔 ∈ (1st ‘1P) ∧ 𝑥 = (𝑓 ·Q 𝑔))))
3231rexbidva 2340 . . . . . 6 ((𝐴P𝑓 ∈ (1st𝐴)) → (∃𝑔 ∈ (1st ‘1P)(𝑥 <Q 𝑓𝑥 = (𝑓 ·Q 𝑔)) ↔ ∃𝑔 ∈ (1st ‘1P)(𝑔 ∈ (1st ‘1P) ∧ 𝑥 = (𝑓 ·Q 𝑔))))
334, 32syl5rbbr 188 . . . . 5 ((𝐴P𝑓 ∈ (1st𝐴)) → (∃𝑔 ∈ (1st ‘1P)(𝑔 ∈ (1st ‘1P) ∧ 𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔))))
343, 33syl5bb 185 . . . 4 ((𝐴P𝑓 ∈ (1st𝐴)) → (∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔))))
3534rexbidva 2340 . . 3 (𝐴P → (∃𝑓 ∈ (1st𝐴)∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔) ↔ ∃𝑓 ∈ (1st𝐴)(𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔))))
36 df-imp 6625 . . . . 5 ·P = (𝑦P, 𝑧P ↦ ⟨{𝑤Q ∣ ∃𝑢Q𝑣Q (𝑢 ∈ (1st𝑦) ∧ 𝑣 ∈ (1st𝑧) ∧ 𝑤 = (𝑢 ·Q 𝑣))}, {𝑤Q ∣ ∃𝑢Q𝑣Q (𝑢 ∈ (2nd𝑦) ∧ 𝑣 ∈ (2nd𝑧) ∧ 𝑤 = (𝑢 ·Q 𝑣))}⟩)
37 mulclnq 6532 . . . . 5 ((𝑢Q𝑣Q) → (𝑢 ·Q 𝑣) ∈ Q)
3836, 37genpelvl 6668 . . . 4 ((𝐴P ∧ 1PP) → (𝑥 ∈ (1st ‘(𝐴 ·P 1P)) ↔ ∃𝑓 ∈ (1st𝐴)∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔)))
395, 38mpan2 409 . . 3 (𝐴P → (𝑥 ∈ (1st ‘(𝐴 ·P 1P)) ↔ ∃𝑓 ∈ (1st𝐴)∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔)))
40 prnmaxl 6644 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑥 ∈ (1st𝐴)) → ∃𝑓 ∈ (1st𝐴)𝑥 <Q 𝑓)
4110, 40sylan 271 . . . . . 6 ((𝐴P𝑥 ∈ (1st𝐴)) → ∃𝑓 ∈ (1st𝐴)𝑥 <Q 𝑓)
42 ltrelnq 6521 . . . . . . . . . . . . 13 <Q ⊆ (Q × Q)
4342brel 4420 . . . . . . . . . . . 12 (𝑥 <Q 𝑓 → (𝑥Q𝑓Q))
44 ltmnqg 6557 . . . . . . . . . . . . . . . 16 ((𝑦Q𝑧Q𝑤Q) → (𝑦 <Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q (𝑤 ·Q 𝑧)))
4544adantl 266 . . . . . . . . . . . . . . 15 (((𝑥Q𝑓Q) ∧ (𝑦Q𝑧Q𝑤Q)) → (𝑦 <Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q (𝑤 ·Q 𝑧)))
46 simpl 106 . . . . . . . . . . . . . . 15 ((𝑥Q𝑓Q) → 𝑥Q)
47 simpr 107 . . . . . . . . . . . . . . 15 ((𝑥Q𝑓Q) → 𝑓Q)
48 recclnq 6548 . . . . . . . . . . . . . . . 16 (𝑓Q → (*Q𝑓) ∈ Q)
4948adantl 266 . . . . . . . . . . . . . . 15 ((𝑥Q𝑓Q) → (*Q𝑓) ∈ Q)
50 mulcomnqg 6539 . . . . . . . . . . . . . . . 16 ((𝑦Q𝑧Q) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦))
5150adantl 266 . . . . . . . . . . . . . . 15 (((𝑥Q𝑓Q) ∧ (𝑦Q𝑧Q)) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦))
5245, 46, 47, 49, 51caovord2d 5698 . . . . . . . . . . . . . 14 ((𝑥Q𝑓Q) → (𝑥 <Q 𝑓 ↔ (𝑥 ·Q (*Q𝑓)) <Q (𝑓 ·Q (*Q𝑓))))
53 recidnq 6549 . . . . . . . . . . . . . . . 16 (𝑓Q → (𝑓 ·Q (*Q𝑓)) = 1Q)
5453breq2d 3804 . . . . . . . . . . . . . . 15 (𝑓Q → ((𝑥 ·Q (*Q𝑓)) <Q (𝑓 ·Q (*Q𝑓)) ↔ (𝑥 ·Q (*Q𝑓)) <Q 1Q))
5554adantl 266 . . . . . . . . . . . . . 14 ((𝑥Q𝑓Q) → ((𝑥 ·Q (*Q𝑓)) <Q (𝑓 ·Q (*Q𝑓)) ↔ (𝑥 ·Q (*Q𝑓)) <Q 1Q))
5652, 55bitrd 181 . . . . . . . . . . . . 13 ((𝑥Q𝑓Q) → (𝑥 <Q 𝑓 ↔ (𝑥 ·Q (*Q𝑓)) <Q 1Q))
5756biimpd 136 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 <Q 𝑓 → (𝑥 ·Q (*Q𝑓)) <Q 1Q))
5843, 57mpcom 36 . . . . . . . . . . 11 (𝑥 <Q 𝑓 → (𝑥 ·Q (*Q𝑓)) <Q 1Q)
59 mulclnq 6532 . . . . . . . . . . . . . 14 ((𝑥Q ∧ (*Q𝑓) ∈ Q) → (𝑥 ·Q (*Q𝑓)) ∈ Q)
6048, 59sylan2 274 . . . . . . . . . . . . 13 ((𝑥Q𝑓Q) → (𝑥 ·Q (*Q𝑓)) ∈ Q)
6143, 60syl 14 . . . . . . . . . . . 12 (𝑥 <Q 𝑓 → (𝑥 ·Q (*Q𝑓)) ∈ Q)
62 breq1 3795 . . . . . . . . . . . . 13 (𝑔 = (𝑥 ·Q (*Q𝑓)) → (𝑔 <Q 1Q ↔ (𝑥 ·Q (*Q𝑓)) <Q 1Q))
6362, 15elab2g 2712 . . . . . . . . . . . 12 ((𝑥 ·Q (*Q𝑓)) ∈ Q → ((𝑥 ·Q (*Q𝑓)) ∈ (1st ‘1P) ↔ (𝑥 ·Q (*Q𝑓)) <Q 1Q))
6461, 63syl 14 . . . . . . . . . . 11 (𝑥 <Q 𝑓 → ((𝑥 ·Q (*Q𝑓)) ∈ (1st ‘1P) ↔ (𝑥 ·Q (*Q𝑓)) <Q 1Q))
6558, 64mpbird 160 . . . . . . . . . 10 (𝑥 <Q 𝑓 → (𝑥 ·Q (*Q𝑓)) ∈ (1st ‘1P))
66 mulassnqg 6540 . . . . . . . . . . . . . 14 ((𝑦Q𝑧Q𝑤Q) → ((𝑦 ·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧 ·Q 𝑤)))
6766adantl 266 . . . . . . . . . . . . 13 (((𝑥Q𝑓Q) ∧ (𝑦Q𝑧Q𝑤Q)) → ((𝑦 ·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧 ·Q 𝑤)))
6847, 46, 49, 51, 67caov12d 5710 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑓 ·Q (𝑥 ·Q (*Q𝑓))) = (𝑥 ·Q (𝑓 ·Q (*Q𝑓))))
6953oveq2d 5556 . . . . . . . . . . . . 13 (𝑓Q → (𝑥 ·Q (𝑓 ·Q (*Q𝑓))) = (𝑥 ·Q 1Q))
7069adantl 266 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q (𝑓 ·Q (*Q𝑓))) = (𝑥 ·Q 1Q))
71 mulidnq 6545 . . . . . . . . . . . . 13 (𝑥Q → (𝑥 ·Q 1Q) = 𝑥)
7271adantr 265 . . . . . . . . . . . 12 ((𝑥Q𝑓Q) → (𝑥 ·Q 1Q) = 𝑥)
7368, 70, 723eqtrrd 2093 . . . . . . . . . . 11 ((𝑥Q𝑓Q) → 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
7443, 73syl 14 . . . . . . . . . 10 (𝑥 <Q 𝑓𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
75 oveq2 5548 . . . . . . . . . . . 12 (𝑔 = (𝑥 ·Q (*Q𝑓)) → (𝑓 ·Q 𝑔) = (𝑓 ·Q (𝑥 ·Q (*Q𝑓))))
7675eqeq2d 2067 . . . . . . . . . . 11 (𝑔 = (𝑥 ·Q (*Q𝑓)) → (𝑥 = (𝑓 ·Q 𝑔) ↔ 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓)))))
7776rspcev 2673 . . . . . . . . . 10 (((𝑥 ·Q (*Q𝑓)) ∈ (1st ‘1P) ∧ 𝑥 = (𝑓 ·Q (𝑥 ·Q (*Q𝑓)))) → ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔))
7865, 74, 77syl2anc 397 . . . . . . . . 9 (𝑥 <Q 𝑓 → ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔))
7978a1i 9 . . . . . . . 8 (𝑓 ∈ (1st𝐴) → (𝑥 <Q 𝑓 → ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔)))
8079ancld 312 . . . . . . 7 (𝑓 ∈ (1st𝐴) → (𝑥 <Q 𝑓 → (𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔))))
8180reximia 2431 . . . . . 6 (∃𝑓 ∈ (1st𝐴)𝑥 <Q 𝑓 → ∃𝑓 ∈ (1st𝐴)(𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔)))
8241, 81syl 14 . . . . 5 ((𝐴P𝑥 ∈ (1st𝐴)) → ∃𝑓 ∈ (1st𝐴)(𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔)))
8382ex 112 . . . 4 (𝐴P → (𝑥 ∈ (1st𝐴) → ∃𝑓 ∈ (1st𝐴)(𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔))))
84 prcdnql 6640 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑓 ∈ (1st𝐴)) → (𝑥 <Q 𝑓𝑥 ∈ (1st𝐴)))
8510, 84sylan 271 . . . . . 6 ((𝐴P𝑓 ∈ (1st𝐴)) → (𝑥 <Q 𝑓𝑥 ∈ (1st𝐴)))
8685adantrd 268 . . . . 5 ((𝐴P𝑓 ∈ (1st𝐴)) → ((𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔)) → 𝑥 ∈ (1st𝐴)))
8786rexlimdva 2450 . . . 4 (𝐴P → (∃𝑓 ∈ (1st𝐴)(𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔)) → 𝑥 ∈ (1st𝐴)))
8883, 87impbid 124 . . 3 (𝐴P → (𝑥 ∈ (1st𝐴) ↔ ∃𝑓 ∈ (1st𝐴)(𝑥 <Q 𝑓 ∧ ∃𝑔 ∈ (1st ‘1P)𝑥 = (𝑓 ·Q 𝑔))))
8935, 39, 883bitr4d 213 . 2 (𝐴P → (𝑥 ∈ (1st ‘(𝐴 ·P 1P)) ↔ 𝑥 ∈ (1st𝐴)))
9089eqrdv 2054 1 (𝐴P → (1st ‘(𝐴 ·P 1P)) = (1st𝐴))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   ∧ w3a 896   = wceq 1259   ∈ wcel 1409  ∃wrex 2324   ⊆ wss 2945  ⟨cop 3406   class class class wbr 3792  ‘cfv 4930  (class class class)co 5540  1st c1st 5793  2nd c2nd 5794  Qcnq 6436  1Qc1q 6437   ·Q cmq 6439  *Qcrq 6440
 Copyright terms: Public domain W3C validator