MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prlem934 Structured version   Visualization version   GIF version

Theorem prlem934 10067
Description: Lemma 9-3.4 of [Gleason] p. 122. (Contributed by NM, 25-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
Hypothesis
Ref Expression
prlem934.1 𝐵 ∈ V
Assertion
Ref Expression
prlem934 (𝐴P → ∃𝑥𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem prlem934
Dummy variables 𝑏 𝑤 𝑦 𝑧 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prn0 10023 . . . . 5 (𝐴P𝐴 ≠ ∅)
2 r19.2z 4204 . . . . . 6 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴) → ∃𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)
32ex 449 . . . . 5 (𝐴 ≠ ∅ → (∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ∃𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
41, 3syl 17 . . . 4 (𝐴P → (∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ∃𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
5 prpssnq 10024 . . . . . . . . 9 (𝐴P𝐴Q)
65pssssd 3846 . . . . . . . 8 (𝐴P𝐴Q)
76sseld 3743 . . . . . . 7 (𝐴P → ((𝑥 +Q 𝐵) ∈ 𝐴 → (𝑥 +Q 𝐵) ∈ Q))
8 addnqf 9982 . . . . . . . . . 10 +Q :(Q × Q)⟶Q
98fdmi 6213 . . . . . . . . 9 dom +Q = (Q × Q)
10 0nnq 9958 . . . . . . . . 9 ¬ ∅ ∈ Q
119, 10ndmovrcl 6986 . . . . . . . 8 ((𝑥 +Q 𝐵) ∈ Q → (𝑥Q𝐵Q))
1211simprd 482 . . . . . . 7 ((𝑥 +Q 𝐵) ∈ Q𝐵Q)
137, 12syl6com 37 . . . . . 6 ((𝑥 +Q 𝐵) ∈ 𝐴 → (𝐴P𝐵Q))
1413rexlimivw 3167 . . . . 5 (∃𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → (𝐴P𝐵Q))
1514com12 32 . . . 4 (𝐴P → (∃𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴𝐵Q))
16 oveq2 6822 . . . . . . . . . 10 (𝑏 = 𝐵 → (𝑥 +Q 𝑏) = (𝑥 +Q 𝐵))
1716eleq1d 2824 . . . . . . . . 9 (𝑏 = 𝐵 → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ (𝑥 +Q 𝐵) ∈ 𝐴))
1817ralbidv 3124 . . . . . . . 8 (𝑏 = 𝐵 → (∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ↔ ∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
1918notbid 307 . . . . . . 7 (𝑏 = 𝐵 → (¬ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ↔ ¬ ∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
2019imbi2d 329 . . . . . 6 (𝑏 = 𝐵 → ((𝐴P → ¬ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ↔ (𝐴P → ¬ ∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)))
21 dfpss2 3834 . . . . . . . . . . 11 (𝐴Q ↔ (𝐴Q ∧ ¬ 𝐴 = Q))
225, 21sylib 208 . . . . . . . . . 10 (𝐴P → (𝐴Q ∧ ¬ 𝐴 = Q))
2322simprd 482 . . . . . . . . 9 (𝐴P → ¬ 𝐴 = Q)
2423adantr 472 . . . . . . . 8 ((𝐴P𝑏Q) → ¬ 𝐴 = Q)
2563ad2ant1 1128 . . . . . . . . . 10 ((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → 𝐴Q)
26 simpl1 1228 . . . . . . . . . . . . . 14 (((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤Q) → 𝐴P)
27 n0 4074 . . . . . . . . . . . . . . 15 (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦𝐴)
281, 27sylib 208 . . . . . . . . . . . . . 14 (𝐴P → ∃𝑦 𝑦𝐴)
2926, 28syl 17 . . . . . . . . . . . . 13 (((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤Q) → ∃𝑦 𝑦𝐴)
30 simprl 811 . . . . . . . . . . . . . . . . 17 (((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) → 𝑤Q)
31 simpl2 1230 . . . . . . . . . . . . . . . . 17 (((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) → 𝑏Q)
32 recclnq 10000 . . . . . . . . . . . . . . . . . 18 (𝑏Q → (*Q𝑏) ∈ Q)
33 mulclnq 9981 . . . . . . . . . . . . . . . . . . 19 ((𝑤Q ∧ (*Q𝑏) ∈ Q) → (𝑤 ·Q (*Q𝑏)) ∈ Q)
34 archnq 10014 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ·Q (*Q𝑏)) ∈ Q → ∃𝑧N (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)
3533, 34syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑤Q ∧ (*Q𝑏) ∈ Q) → ∃𝑧N (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)
3632, 35sylan2 492 . . . . . . . . . . . . . . . . 17 ((𝑤Q𝑏Q) → ∃𝑧N (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)
3730, 31, 36syl2anc 696 . . . . . . . . . . . . . . . 16 (((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) → ∃𝑧N (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)
38 simpll2 1257 . . . . . . . . . . . . . . . . . . 19 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → 𝑏Q)
39 simplrl 819 . . . . . . . . . . . . . . . . . . 19 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → 𝑤Q)
40 simprr 813 . . . . . . . . . . . . . . . . . . 19 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)
41 ltmnq 10006 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏Q → ((𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩ ↔ (𝑏 ·Q (𝑤 ·Q (*Q𝑏))) <Q (𝑏 ·Q𝑧, 1𝑜⟩)))
42 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏 ∈ V
43 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤 ∈ V
44 fvex 6363 . . . . . . . . . . . . . . . . . . . . . . . . 25 (*Q𝑏) ∈ V
45 mulcomnq 9987 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 ·Q 𝑥) = (𝑥 ·Q 𝑣)
46 mulassnq 9993 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 ·Q 𝑥) ·Q 𝑦) = (𝑣 ·Q (𝑥 ·Q 𝑦))
4742, 43, 44, 45, 46caov12 7028 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 ·Q (𝑤 ·Q (*Q𝑏))) = (𝑤 ·Q (𝑏 ·Q (*Q𝑏)))
48 mulcomnq 9987 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 ·Q𝑧, 1𝑜⟩) = (⟨𝑧, 1𝑜⟩ ·Q 𝑏)
4947, 48breq12i 4813 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 ·Q (𝑤 ·Q (*Q𝑏))) <Q (𝑏 ·Q𝑧, 1𝑜⟩) ↔ (𝑤 ·Q (𝑏 ·Q (*Q𝑏))) <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏))
5041, 49syl6bb 276 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏Q → ((𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩ ↔ (𝑤 ·Q (𝑏 ·Q (*Q𝑏))) <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
5150adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏Q𝑤Q) → ((𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩ ↔ (𝑤 ·Q (𝑏 ·Q (*Q𝑏))) <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
52 recidnq 9999 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏Q → (𝑏 ·Q (*Q𝑏)) = 1Q)
5352oveq2d 6830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏Q → (𝑤 ·Q (𝑏 ·Q (*Q𝑏))) = (𝑤 ·Q 1Q))
54 mulidnq 9997 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤Q → (𝑤 ·Q 1Q) = 𝑤)
5553, 54sylan9eq 2814 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏Q𝑤Q) → (𝑤 ·Q (𝑏 ·Q (*Q𝑏))) = 𝑤)
5655breq1d 4814 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏Q𝑤Q) → ((𝑤 ·Q (𝑏 ·Q (*Q𝑏))) <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏) ↔ 𝑤 <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
5751, 56bitrd 268 . . . . . . . . . . . . . . . . . . . 20 ((𝑏Q𝑤Q) → ((𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩ ↔ 𝑤 <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
5857biimpa 502 . . . . . . . . . . . . . . . . . . 19 (((𝑏Q𝑤Q) ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩) → 𝑤 <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏))
5938, 39, 40, 58syl21anc 1476 . . . . . . . . . . . . . . . . . 18 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → 𝑤 <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏))
60 simprl 811 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → 𝑧N)
61 pinq 9961 . . . . . . . . . . . . . . . . . . . . 21 (𝑧N → ⟨𝑧, 1𝑜⟩ ∈ Q)
62 mulclnq 9981 . . . . . . . . . . . . . . . . . . . . 21 ((⟨𝑧, 1𝑜⟩ ∈ Q𝑏Q) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∈ Q)
6361, 62sylan 489 . . . . . . . . . . . . . . . . . . . 20 ((𝑧N𝑏Q) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∈ Q)
6460, 38, 63syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∈ Q)
65 simpll1 1255 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → 𝐴P)
66 simplrr 820 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → 𝑦𝐴)
67 elprnq 10025 . . . . . . . . . . . . . . . . . . . 20 ((𝐴P𝑦𝐴) → 𝑦Q)
6865, 66, 67syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → 𝑦Q)
69 ltaddnq 10008 . . . . . . . . . . . . . . . . . . . 20 (((⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∈ Q𝑦Q) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) <Q ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑦))
70 addcomnq 9985 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑦) = (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏))
7169, 70syl6breq 4845 . . . . . . . . . . . . . . . . . . 19 (((⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∈ Q𝑦Q) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
7264, 68, 71syl2anc 696 . . . . . . . . . . . . . . . . . 18 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
73 ltsonq 10003 . . . . . . . . . . . . . . . . . . 19 <Q Or Q
74 ltrelnq 9960 . . . . . . . . . . . . . . . . . . 19 <Q ⊆ (Q × Q)
7573, 74sotri 5681 . . . . . . . . . . . . . . . . . 18 ((𝑤 <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∧ (⟨𝑧, 1𝑜⟩ ·Q 𝑏) <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏))) → 𝑤 <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
7659, 72, 75syl2anc 696 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → 𝑤 <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
77 simpll3 1259 . . . . . . . . . . . . . . . . . . 19 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴)
78 opeq1 4553 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 1𝑜 → ⟨𝑤, 1𝑜⟩ = ⟨1𝑜, 1𝑜⟩)
79 df-1nq 9950 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1Q = ⟨1𝑜, 1𝑜
8078, 79syl6eqr 2812 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 1𝑜 → ⟨𝑤, 1𝑜⟩ = 1Q)
8180oveq1d 6829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 1𝑜 → (⟨𝑤, 1𝑜⟩ ·Q 𝑏) = (1Q ·Q 𝑏))
8281oveq2d 6830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 1𝑜 → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) = (𝑦 +Q (1Q ·Q 𝑏)))
8382eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 1𝑜 → ((𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴))
8483imbi2d 329 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 1𝑜 → (((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴)))
85 opeq1 4553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑧 → ⟨𝑤, 1𝑜⟩ = ⟨𝑧, 1𝑜⟩)
8685oveq1d 6829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑧 → (⟨𝑤, 1𝑜⟩ ·Q 𝑏) = (⟨𝑧, 1𝑜⟩ ·Q 𝑏))
8786oveq2d 6830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) = (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
8887eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → ((𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴))
8988imbi2d 329 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
90 opeq1 4553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = (𝑧 +N 1𝑜) → ⟨𝑤, 1𝑜⟩ = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
9190oveq1d 6829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑧 +N 1𝑜) → (⟨𝑤, 1𝑜⟩ ·Q 𝑏) = (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏))
9291oveq2d 6830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑧 +N 1𝑜) → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) = (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)))
9392eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝑧 +N 1𝑜) → ((𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴))
9493imbi2d 329 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝑧 +N 1𝑜) → (((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
95 mulcomnq 9987 . . . . . . . . . . . . . . . . . . . . . . . 24 (1Q ·Q 𝑏) = (𝑏 ·Q 1Q)
96 mulidnq 9997 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏Q → (𝑏 ·Q 1Q) = 𝑏)
9795, 96syl5eq 2806 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏Q → (1Q ·Q 𝑏) = 𝑏)
98 oveq1 6821 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑦 → (𝑥 +Q 𝑏) = (𝑦 +Q 𝑏))
9998eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ (𝑦 +Q 𝑏) ∈ 𝐴))
10099rspccva 3448 . . . . . . . . . . . . . . . . . . . . . . 23 ((∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q 𝑏) ∈ 𝐴)
101 oveq2 6822 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1Q ·Q 𝑏) = 𝑏 → (𝑦 +Q (1Q ·Q 𝑏)) = (𝑦 +Q 𝑏))
102101eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1Q ·Q 𝑏) = 𝑏 → ((𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q 𝑏) ∈ 𝐴))
103102biimpar 503 . . . . . . . . . . . . . . . . . . . . . . 23 (((1Q ·Q 𝑏) = 𝑏 ∧ (𝑦 +Q 𝑏) ∈ 𝐴) → (𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴)
10497, 100, 103syl2an 495 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏Q ∧ (∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴)) → (𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴)
1051043impb 1108 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴)
106 3simpa 1143 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴))
107 oveq1 6821 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) → (𝑥 +Q 𝑏) = ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏))
108107eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏) ∈ 𝐴))
109108rspccva 3448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) → ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏) ∈ 𝐴)
110 addassnq 9992 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏) = (𝑦 +Q ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑏))
111 opex 5081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑧, 1𝑜⟩ ∈ V
112 1nq 9962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 1QQ
113112elexi 3353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 1Q ∈ V
114 distrnq 9995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ·Q (𝑥 +Q 𝑦)) = ((𝑣 ·Q 𝑥) +Q (𝑣 ·Q 𝑦))
115111, 113, 42, 45, 114caovdir 7034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((⟨𝑧, 1𝑜⟩ +Q 1Q) ·Q 𝑏) = ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q (1Q ·Q 𝑏))
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧N𝑏Q) → ((⟨𝑧, 1𝑜⟩ +Q 1Q) ·Q 𝑏) = ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q (1Q ·Q 𝑏)))
117 addpqnq 9972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((⟨𝑧, 1𝑜⟩ ∈ Q ∧ 1QQ) → (⟨𝑧, 1𝑜⟩ +Q 1Q) = ([Q]‘(⟨𝑧, 1𝑜⟩ +pQ 1Q)))
11861, 112, 117sylancl 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧N → (⟨𝑧, 1𝑜⟩ +Q 1Q) = ([Q]‘(⟨𝑧, 1𝑜⟩ +pQ 1Q)))
11979oveq2i 6825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (⟨𝑧, 1𝑜⟩ +pQ 1Q) = (⟨𝑧, 1𝑜⟩ +pQ ⟨1𝑜, 1𝑜⟩)
120 1pi 9917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1𝑜N
121 addpipq 9971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑧N ∧ 1𝑜N) ∧ (1𝑜N ∧ 1𝑜N)) → (⟨𝑧, 1𝑜⟩ +pQ ⟨1𝑜, 1𝑜⟩) = ⟨((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩)
122120, 120, 121mpanr12 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑧N ∧ 1𝑜N) → (⟨𝑧, 1𝑜⟩ +pQ ⟨1𝑜, 1𝑜⟩) = ⟨((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩)
123120, 122mpan2 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧N → (⟨𝑧, 1𝑜⟩ +pQ ⟨1𝑜, 1𝑜⟩) = ⟨((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩)
124119, 123syl5eq 2806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧N → (⟨𝑧, 1𝑜⟩ +pQ 1Q) = ⟨((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩)
125 mulidpi 9920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧N → (𝑧 ·N 1𝑜) = 𝑧)
126 mulidpi 9920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (1𝑜N → (1𝑜 ·N 1𝑜) = 1𝑜)
127120, 126mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧N → (1𝑜 ·N 1𝑜) = 1𝑜)
128125, 127oveq12d 6832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧N → ((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)) = (𝑧 +N 1𝑜))
129128, 127opeq12d 4561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧N → ⟨((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩ = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
130124, 129eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧N → (⟨𝑧, 1𝑜⟩ +pQ 1Q) = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
131130fveq2d 6357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧N → ([Q]‘(⟨𝑧, 1𝑜⟩ +pQ 1Q)) = ([Q]‘⟨(𝑧 +N 1𝑜), 1𝑜⟩))
132 addclpi 9926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑧N ∧ 1𝑜N) → (𝑧 +N 1𝑜) ∈ N)
133120, 132mpan2 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧N → (𝑧 +N 1𝑜) ∈ N)
134 pinq 9961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑧 +N 1𝑜) ∈ N → ⟨(𝑧 +N 1𝑜), 1𝑜⟩ ∈ Q)
135 nqerid 9967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ∈ Q → ([Q]‘⟨(𝑧 +N 1𝑜), 1𝑜⟩) = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
136133, 134, 1353syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧N → ([Q]‘⟨(𝑧 +N 1𝑜), 1𝑜⟩) = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
137118, 131, 1363eqtrd 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧N → (⟨𝑧, 1𝑜⟩ +Q 1Q) = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
138137adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧N𝑏Q) → (⟨𝑧, 1𝑜⟩ +Q 1Q) = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
139138oveq1d 6829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧N𝑏Q) → ((⟨𝑧, 1𝑜⟩ +Q 1Q) ·Q 𝑏) = (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏))
14097adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧N𝑏Q) → (1Q ·Q 𝑏) = 𝑏)
141140oveq2d 6830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧N𝑏Q) → ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q (1Q ·Q 𝑏)) = ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑏))
142116, 139, 1413eqtr3rd 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧N𝑏Q) → ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑏) = (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏))
143142oveq2d 6830 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑧N𝑏Q) → (𝑦 +Q ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑏)) = (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)))
144110, 143syl5eq 2806 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑧N𝑏Q) → ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏) = (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)))
145144eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧N𝑏Q) → (((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏) ∈ 𝐴 ↔ (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴))
146109, 145syl5ib 234 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧N𝑏Q) → ((∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴))
147146expd 451 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧N𝑏Q) → (∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 → ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
148147expimpd 630 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧N → ((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
149106, 148syl5 34 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧N → ((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
150149a2d 29 . . . . . . . . . . . . . . . . . . . . 21 (𝑧N → (((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) → ((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
15184, 89, 94, 89, 105, 150indpi 9941 . . . . . . . . . . . . . . . . . . . 20 (𝑧N → ((𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴) → (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴))
152151imp 444 . . . . . . . . . . . . . . . . . . 19 ((𝑧N ∧ (𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝑦𝐴)) → (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)
15360, 38, 77, 66, 152syl13anc 1479 . . . . . . . . . . . . . . . . . 18 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)
154 prcdnq 10027 . . . . . . . . . . . . . . . . . 18 ((𝐴P ∧ (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) → (𝑤 <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) → 𝑤𝐴))
15565, 153, 154syl2anc 696 . . . . . . . . . . . . . . . . 17 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → (𝑤 <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) → 𝑤𝐴))
15676, 155mpd 15 . . . . . . . . . . . . . . . 16 ((((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) ∧ (𝑧N ∧ (𝑤 ·Q (*Q𝑏)) <Q𝑧, 1𝑜⟩)) → 𝑤𝐴)
15737, 156rexlimddv 3173 . . . . . . . . . . . . . . 15 (((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤Q𝑦𝐴)) → 𝑤𝐴)
158157expr 644 . . . . . . . . . . . . . 14 (((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤Q) → (𝑦𝐴𝑤𝐴))
159158exlimdv 2010 . . . . . . . . . . . . 13 (((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤Q) → (∃𝑦 𝑦𝐴𝑤𝐴))
16029, 159mpd 15 . . . . . . . . . . . 12 (((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤Q) → 𝑤𝐴)
161160ex 449 . . . . . . . . . . 11 ((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → (𝑤Q𝑤𝐴))
162161ssrdv 3750 . . . . . . . . . 10 ((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → Q𝐴)
16325, 162eqssd 3761 . . . . . . . . 9 ((𝐴P𝑏Q ∧ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → 𝐴 = Q)
1641633expia 1115 . . . . . . . 8 ((𝐴P𝑏Q) → (∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴𝐴 = Q))
16524, 164mtod 189 . . . . . . 7 ((𝐴P𝑏Q) → ¬ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴)
166165expcom 450 . . . . . 6 (𝑏Q → (𝐴P → ¬ ∀𝑥𝐴 (𝑥 +Q 𝑏) ∈ 𝐴))
16720, 166vtoclga 3412 . . . . 5 (𝐵Q → (𝐴P → ¬ ∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
168167com12 32 . . . 4 (𝐴P → (𝐵Q → ¬ ∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
1694, 15, 1683syld 60 . . 3 (𝐴P → (∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ¬ ∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
170169pm2.01d 181 . 2 (𝐴P → ¬ ∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)
171 rexnal 3133 . 2 (∃𝑥𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴 ↔ ¬ ∀𝑥𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)
172170, 171sylibr 224 1 (𝐴P → ∃𝑥𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wex 1853  wcel 2139  wne 2932  wral 3050  wrex 3051  Vcvv 3340  wss 3715  wpss 3716  c0 4058  cop 4327   class class class wbr 4804   × cxp 5264  cfv 6049  (class class class)co 6814  1𝑜c1o 7723  Ncnpi 9878   +N cpli 9879   ·N cmi 9880   +pQ cplpq 9882  Qcnq 9886  1Qc1q 9887  [Q]cerq 9888   +Q cplq 9889   ·Q cmq 9890  *Qcrq 9891   <Q cltq 9892  Pcnp 9893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-oadd 7734  df-omul 7735  df-er 7913  df-ni 9906  df-pli 9907  df-mi 9908  df-lti 9909  df-plpq 9942  df-mpq 9943  df-ltpq 9944  df-enq 9945  df-nq 9946  df-erq 9947  df-plq 9948  df-mq 9949  df-1nq 9950  df-rq 9951  df-ltnq 9952  df-np 10015
This theorem is referenced by:  ltaddpr  10068  ltexprlem7  10076  prlem936  10081
  Copyright terms: Public domain W3C validator