recexprlemopl - Intuitionistic Logic Explorer

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

Theorem recexprlemopl 7720

Description: The lower cut of 𝐵 is open. Lemma for recexpr 7733. (Contributed by Jim Kingdon, 28-Dec-2019.)

**Hypothesis**
Ref	Expression
recexpr.1	⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <_Q 𝑦 ∧ (_Q‘𝑦) ∈ (2^nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <_Q 𝑥 ∧ (_Q‘𝑦) ∈ (1^st ‘𝐴))}⟩

**Assertion**
Ref	Expression
recexprlemopl	⊢ ((𝐴 ∈ P ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1^st ‘𝐵)) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵)))

Distinct variable groups: 𝑟,𝑞,𝑥,𝑦,𝐴 𝐵,𝑞,𝑟,𝑥,𝑦

**Proof of Theorem recexprlemopl**
Step	Hyp	Ref	Expression
1		recexpr.1	. . . 4 ⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <_Q 𝑦 ∧ (_Q‘𝑦) ∈ (2^nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <_Q 𝑥 ∧ (_Q‘𝑦) ∈ (1^st ‘𝐴))}⟩
2	1	recexprlemell 7717	. . 3 ⊢ (𝑞 ∈ (1^st ‘𝐵) ↔ ∃𝑦(𝑞 <_Q 𝑦 ∧ (*_Q‘𝑦) ∈ (2^nd ‘𝐴)))
3		ltbtwnnqq 7510	. . . . . 6 ⊢ (𝑞 <_Q 𝑦 ↔ ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 <_Q 𝑦))
4	3	biimpi 120	. . . . 5 ⊢ (𝑞 <_Q 𝑦 → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 <_Q 𝑦))
5		simpll 527	. . . . . . . 8 ⊢ (((𝑞 <_Q 𝑟 ∧ 𝑟 <_Q 𝑦) ∧ (*_Q‘𝑦) ∈ (2^nd ‘𝐴)) → 𝑞 <_Q 𝑟)
6		19.8a 1612	. . . . . . . . . 10 ⊢ ((𝑟 <_Q 𝑦 ∧ (_Q‘𝑦) ∈ (2^nd ‘𝐴)) → ∃𝑦(𝑟 <_Q 𝑦 ∧ (_Q‘𝑦) ∈ (2^nd ‘𝐴)))
7	1	recexprlemell 7717	. . . . . . . . . 10 ⊢ (𝑟 ∈ (1^st ‘𝐵) ↔ ∃𝑦(𝑟 <_Q 𝑦 ∧ (*_Q‘𝑦) ∈ (2^nd ‘𝐴)))
8	6, 7	sylibr 134	. . . . . . . . 9 ⊢ ((𝑟 <_Q 𝑦 ∧ (*_Q‘𝑦) ∈ (2^nd ‘𝐴)) → 𝑟 ∈ (1^st ‘𝐵))
9	8	adantll 476	. . . . . . . 8 ⊢ (((𝑞 <_Q 𝑟 ∧ 𝑟 <_Q 𝑦) ∧ (*_Q‘𝑦) ∈ (2^nd ‘𝐴)) → 𝑟 ∈ (1^st ‘𝐵))
10	5, 9	jca 306	. . . . . . 7 ⊢ (((𝑞 <_Q 𝑟 ∧ 𝑟 <_Q 𝑦) ∧ (*_Q‘𝑦) ∈ (2^nd ‘𝐴)) → (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵)))
11	10	expcom 116	. . . . . 6 ⊢ ((*_Q‘𝑦) ∈ (2^nd ‘𝐴) → ((𝑞 <_Q 𝑟 ∧ 𝑟 <_Q 𝑦) → (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵))))
12	11	reximdv 2606	. . . . 5 ⊢ ((*_Q‘𝑦) ∈ (2^nd ‘𝐴) → (∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 <_Q 𝑦) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵))))
13	4, 12	mpan9 281	. . . 4 ⊢ ((𝑞 <_Q 𝑦 ∧ (*_Q‘𝑦) ∈ (2^nd ‘𝐴)) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵)))
14	13	exlimiv 1620	. . 3 ⊢ (∃𝑦(𝑞 <_Q 𝑦 ∧ (*_Q‘𝑦) ∈ (2^nd ‘𝐴)) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵)))
15	2, 14	sylbi 121	. 2 ⊢ (𝑞 ∈ (1^st ‘𝐵) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵)))
16	15	3ad2ant3 1022	1 ⊢ ((𝐴 ∈ P ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1^st ‘𝐵)) → ∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 = wceq 1372 ∃wex 1514 ∈ wcel 2175 {cab 2190 ∃wrex 2484 ⟨cop 3635 class class class wbr 4043 ‘cfv 5268 1^st c1st 6214 2^nd c2nd 6215 Qcnq 7375 *_Qcrq 7379 <_Q cltq 7380 Pcnp 7386

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 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-coll 4158 ax-sep 4161 ax-nul 4169 ax-pow 4217 ax-pr 4252 ax-un 4478 ax-setind 4583 ax-iinf 4634

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-ral 2488 df-rex 2489 df-reu 2490 df-rab 2492 df-v 2773 df-sbc 2998 df-csb 3093 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-iun 3928 df-br 4044 df-opab 4105 df-mpt 4106 df-tr 4142 df-eprel 4334 df-id 4338 df-po 4341 df-iso 4342 df-iord 4411 df-on 4413 df-suc 4416 df-iom 4637 df-xp 4679 df-rel 4680 df-cnv 4681 df-co 4682 df-dm 4683 df-rn 4684 df-res 4685 df-ima 4686 df-iota 5229 df-fun 5270 df-fn 5271 df-f 5272 df-f1 5273 df-fo 5274 df-f1o 5275 df-fv 5276 df-ov 5937 df-oprab 5938 df-mpo 5939 df-1st 6216 df-2nd 6217 df-recs 6381 df-irdg 6446 df-1o 6492 df-oadd 6496 df-omul 6497 df-er 6610 df-ec 6612 df-qs 6616 df-ni 7399 df-pli 7400 df-mi 7401 df-lti 7402 df-plpq 7439 df-mpq 7440 df-enq 7442 df-nqqs 7443 df-plqqs 7444 df-mqqs 7445 df-1nqqs 7446 df-rq 7447 df-ltnqqs 7448

This theorem is referenced by: recexprlemrnd 7724

W3C validator