suplocexprlem2b - Intuitionistic Logic Explorer

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

Theorem suplocexprlem2b 7889

Description: Lemma for suplocexpr 7900. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)

**Hypothesis**
Ref	Expression
suplocexprlem2b.b	⊢ 𝐵 = ⟨∪ (1^st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢}⟩

**Assertion**
Ref	Expression
suplocexprlem2b	⊢ (𝐴 ⊆ P → (2^nd ‘𝐵) = {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢})

**Proof of Theorem suplocexprlem2b**
Step	Hyp	Ref	Expression
1		suplocexprlem2b.b	. . 3 ⊢ 𝐵 = ⟨∪ (1^st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢}⟩
2	1	fveq2i 5626	. 2 ⊢ (2^nd ‘𝐵) = (2^nd ‘⟨∪ (1^st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢}⟩)
3		fo1st 6293	. . . . . 6 ⊢ 1^st :V–onto→V
4		fofun 5545	. . . . . 6 ⊢ (1^st :V–onto→V → Fun 1^st )
5	3, 4	ax-mp 5	. . . . 5 ⊢ Fun 1^st
6		npex 7648	. . . . . 6 ⊢ P ∈ V
7	6	ssex 4220	. . . . 5 ⊢ (𝐴 ⊆ P → 𝐴 ∈ V)
8		funimaexg 5401	. . . . 5 ⊢ ((Fun 1^st ∧ 𝐴 ∈ V) → (1^st “ 𝐴) ∈ V)
9	5, 7, 8	sylancr 414	. . . 4 ⊢ (𝐴 ⊆ P → (1^st “ 𝐴) ∈ V)
10		uniexg 4527	. . . 4 ⊢ ((1^st “ 𝐴) ∈ V → ∪ (1^st “ 𝐴) ∈ V)
11	9, 10	syl 14	. . 3 ⊢ (𝐴 ⊆ P → ∪ (1^st “ 𝐴) ∈ V)
12		nqex 7538	. . . 4 ⊢ Q ∈ V
13	12	rabex 4227	. . 3 ⊢ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢} ∈ V
14		op2ndg 6287	. . 3 ⊢ ((∪ (1^st “ 𝐴) ∈ V ∧ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢} ∈ V) → (2^nd ‘⟨∪ (1^st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢}⟩) = {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢})
15	11, 13, 14	sylancl 413	. 2 ⊢ (𝐴 ⊆ P → (2^nd ‘⟨∪ (1^st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢}⟩) = {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢})
16	2, 15	eqtrid 2274	1 ⊢ (𝐴 ⊆ P → (2^nd ‘𝐵) = {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢})

Colors of variables: wff set class

Syntax hints: → wi 4 = wceq 1395 ∈ wcel 2200 ∃wrex 2509 {crab 2512 Vcvv 2799 ⊆ wss 3197 ⟨cop 3669 ∪ cuni 3887 ∩ cint 3922 class class class wbr 4082 “ cima 4719 Fun wfun 5308 –onto→wfo 5312 ‘cfv 5314 1^st c1st 6274 2^nd c2nd 6275 Qcnq 7455 <_Q cltq 7460 Pcnp 7466

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-pow 4257 ax-pr 4292 ax-un 4521 ax-iinf 4677

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-reu 2515 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-br 4083 df-opab 4145 df-mpt 4146 df-id 4381 df-iom 4680 df-xp 4722 df-rel 4723 df-cnv 4724 df-co 4725 df-dm 4726 df-rn 4727 df-res 4728 df-ima 4729 df-iota 5274 df-fun 5316 df-fn 5317 df-f 5318 df-f1 5319 df-fo 5320 df-f1o 5321 df-fv 5322 df-1st 6276 df-2nd 6277 df-qs 6676 df-ni 7479 df-nqqs 7523 df-inp 7641

This theorem is referenced by: suplocexprlemmu 7893 suplocexprlemru 7894 suplocexprlemdisj 7895 suplocexprlemloc 7896 suplocexprlemex 7897 suplocexprlemub 7898

W3C validator