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
 Copyright terms: Public domain W3C validator