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

Theorem caucvgprprlemnjltk 6846
Description: Lemma for caucvgprpr 6867. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.)
Hypotheses
Ref Expression
caucvgprpr.f (𝜑𝐹:NP)
caucvgprpr.cau (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
caucvgprprlemnkj.k (𝜑𝐾N)
caucvgprprlemnkj.j (𝜑𝐽N)
caucvgprprlemnkj.s (𝜑𝑆Q)
Assertion
Ref Expression
caucvgprprlemnjltk ((𝜑𝐽 <N 𝐾) → ¬ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩))
Distinct variable groups:   𝑘,𝐹,𝑛   𝐽,𝑙,𝑝   𝐽,𝑞,𝑢   𝐾,𝑝   𝐾,𝑞   𝑆,𝑝   𝑆,𝑞   𝑢,𝑘   𝑘,𝑙,𝑛   𝑢,𝑛
Allowed substitution hints:   𝜑(𝑢,𝑘,𝑛,𝑞,𝑝,𝑙)   𝑆(𝑢,𝑘,𝑛,𝑙)   𝐹(𝑢,𝑞,𝑝,𝑙)   𝐽(𝑘,𝑛)   𝐾(𝑢,𝑘,𝑛,𝑙)

Proof of Theorem caucvgprprlemnjltk
StepHypRef Expression
1 ltsopr 6751 . . 3 <P Or P
2 ltrelpr 6660 . . 3 <P ⊆ (P × P)
31, 2son2lpi 4748 . 2 ¬ (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)
4 caucvgprprlemnkj.s . . . . . . . 8 (𝜑𝑆Q)
54ad2antrr 465 . . . . . . 7 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → 𝑆Q)
6 caucvgprprlemnkj.k . . . . . . . . 9 (𝜑𝐾N)
76ad2antrr 465 . . . . . . . 8 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → 𝐾N)
8 nnnq 6577 . . . . . . . 8 (𝐾N → [⟨𝐾, 1𝑜⟩] ~QQ)
9 recclnq 6547 . . . . . . . 8 ([⟨𝐾, 1𝑜⟩] ~QQ → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) ∈ Q)
107, 8, 93syl 17 . . . . . . 7 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) ∈ Q)
11 ltaddnq 6562 . . . . . . 7 ((𝑆Q ∧ (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ) ∈ Q) → 𝑆 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )))
125, 10, 11syl2anc 397 . . . . . 6 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → 𝑆 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )))
13 ltnqpri 6749 . . . . . 6 (𝑆 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) → ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
1412, 13syl 14 . . . . 5 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩)
15 simprl 491 . . . . . 6 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾))
16 caucvgprpr.f . . . . . . . . 9 (𝜑𝐹:NP)
17 caucvgprpr.cau . . . . . . . . 9 (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐹𝑛)<P ((𝐹𝑘) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹𝑘)<P ((𝐹𝑛) +P ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1𝑜⟩] ~Q ) <Q 𝑢}⟩))))
1816, 17caucvgprprlemval 6843 . . . . . . . 8 ((𝜑𝐽 <N 𝐾) → ((𝐹𝐽)<P ((𝐹𝐾) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ (𝐹𝐾)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)))
1918simprd 111 . . . . . . 7 ((𝜑𝐽 <N 𝐾) → (𝐹𝐾)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
2019adantr 265 . . . . . 6 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (𝐹𝐾)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
211, 2sotri 4747 . . . . . 6 ((⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ (𝐹𝐾)<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
2215, 20, 21syl2anc 397 . . . . 5 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
231, 2sotri 4747 . . . . 5 ((⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P ⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩ ∧ ⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
2414, 22, 23syl2anc 397 . . . 4 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩))
25 simprr 492 . . . 4 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)
2624, 25jca 294 . . 3 (((𝜑𝐽 <N 𝐾) ∧ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)) → (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩))
2726ex 112 . 2 ((𝜑𝐽 <N 𝐾) → ((⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩) → (⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩<P ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩)))
283, 27mtoi 600 1 ((𝜑𝐽 <N 𝐾) → ¬ (⟨{𝑝𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1𝑜⟩] ~Q )) <Q 𝑞}⟩<P (𝐹𝐾) ∧ ((𝐹𝐽) +P ⟨{𝑝𝑝 <Q (*Q‘[⟨𝐽, 1𝑜⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1𝑜⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝𝑝 <Q 𝑆}, {𝑞𝑆 <Q 𝑞}⟩))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 101  wcel 1409  {cab 2042  wral 2323  cop 3405   class class class wbr 3791  wf 4925  cfv 4929  (class class class)co 5539  1𝑜c1o 6024  [cec 6134  Ncnpi 6427   <N clti 6430   ~Q ceq 6434  Qcnq 6435   +Q cplq 6437  *Qcrq 6439   <Q cltq 6440  Pcnp 6446   +P cpp 6448  <P cltp 6450
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-coll 3899  ax-sep 3902  ax-nul 3910  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-setind 4289  ax-iinf 4338
This theorem depends on definitions:  df-bi 114  df-dc 754  df-3or 897  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-int 3643  df-iun 3686  df-br 3792  df-opab 3846  df-mpt 3847  df-tr 3882  df-eprel 4053  df-id 4057  df-po 4060  df-iso 4061  df-iord 4130  df-on 4132  df-suc 4135  df-iom 4341  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937  df-ov 5542  df-oprab 5543  df-mpt2 5544  df-1st 5794  df-2nd 5795  df-recs 5950  df-irdg 5987  df-1o 6031  df-oadd 6035  df-omul 6036  df-er 6136  df-ec 6138  df-qs 6142  df-ni 6459  df-pli 6460  df-mi 6461  df-lti 6462  df-plpq 6499  df-mpq 6500  df-enq 6502  df-nqqs 6503  df-plqqs 6504  df-mqqs 6505  df-1nqqs 6506  df-rq 6507  df-ltnqqs 6508  df-inp 6621  df-iltp 6625
This theorem is referenced by:  caucvgprprlemnkj  6847
  Copyright terms: Public domain W3C validator