recexprlemlol - Intuitionistic Logic Explorer

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

Theorem recexprlemlol 7889

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

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

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

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

**Proof of Theorem recexprlemlol**
Step	Hyp	Ref	Expression
1		ltsonq 7661	. . . . . . . . 9 ⊢ <_Q Or Q
2		ltrelnq 7628	. . . . . . . . 9 ⊢ <_Q ⊆ (Q × Q)
3	1, 2	sotri 5139	. . . . . . . 8 ⊢ ((𝑞 <_Q 𝑟 ∧ 𝑟 <_Q 𝑦) → 𝑞 <_Q 𝑦)
4	3	ex 115	. . . . . . 7 ⊢ (𝑞 <_Q 𝑟 → (𝑟 <_Q 𝑦 → 𝑞 <_Q 𝑦))
5	4	anim1d 336	. . . . . 6 ⊢ (𝑞 <_Q 𝑟 → ((𝑟 <_Q 𝑦 ∧ (_Q‘𝑦) ∈ (2^nd ‘𝐴)) → (𝑞 <_Q 𝑦 ∧ (_Q‘𝑦) ∈ (2^nd ‘𝐴))))
6	5	eximdv 1928	. . . . 5 ⊢ (𝑞 <_Q 𝑟 → (∃𝑦(𝑟 <_Q 𝑦 ∧ (_Q‘𝑦) ∈ (2^nd ‘𝐴)) → ∃𝑦(𝑞 <_Q 𝑦 ∧ (_Q‘𝑦) ∈ (2^nd ‘𝐴))))
7		recexpr.1	. . . . . 6 ⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <_Q 𝑦 ∧ (_Q‘𝑦) ∈ (2^nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <_Q 𝑥 ∧ (_Q‘𝑦) ∈ (1^st ‘𝐴))}⟩
8	7	recexprlemell 7885	. . . . 5 ⊢ (𝑟 ∈ (1^st ‘𝐵) ↔ ∃𝑦(𝑟 <_Q 𝑦 ∧ (*_Q‘𝑦) ∈ (2^nd ‘𝐴)))
9	7	recexprlemell 7885	. . . . 5 ⊢ (𝑞 ∈ (1^st ‘𝐵) ↔ ∃𝑦(𝑞 <_Q 𝑦 ∧ (*_Q‘𝑦) ∈ (2^nd ‘𝐴)))
10	6, 8, 9	3imtr4g 205	. . . 4 ⊢ (𝑞 <_Q 𝑟 → (𝑟 ∈ (1^st ‘𝐵) → 𝑞 ∈ (1^st ‘𝐵)))
11	10	imp 124	. . 3 ⊢ ((𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵)) → 𝑞 ∈ (1^st ‘𝐵))
12	11	rexlimivw 2647	. 2 ⊢ (∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵)) → 𝑞 ∈ (1^st ‘𝐵))
13	12	a1i 9	1 ⊢ ((𝐴 ∈ P ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <_Q 𝑟 ∧ 𝑟 ∈ (1^st ‘𝐵)) → 𝑞 ∈ (1^st ‘𝐵)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1398 ∃wex 1541 ∈ wcel 2202 {cab 2217 ∃wrex 2512 ⟨cop 3676 class class class wbr 4093 ‘cfv 5333 1^st c1st 6310 2^nd c2nd 6311 Qcnq 7543 *_Qcrq 7547 <_Q cltq 7548 Pcnp 7554

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-ral 2516 df-rex 2517 df-reu 2518 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-eprel 4392 df-id 4396 df-po 4399 df-iso 4400 df-iord 4469 df-on 4471 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-ov 6031 df-oprab 6032 df-mpo 6033 df-1st 6312 df-2nd 6313 df-recs 6514 df-irdg 6579 df-oadd 6629 df-omul 6630 df-er 6745 df-ec 6747 df-qs 6751 df-ni 7567 df-mi 7569 df-lti 7570 df-enq 7610 df-nqqs 7611 df-ltnqqs 7616

This theorem is referenced by: recexprlemrnd 7892

W3C validator