suplocexprlem2b - Intuitionistic Logic Explorer

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

Theorem suplocexprlem2b 7709

Description: Lemma for suplocexpr 7720. 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 5516	. 2 ⊢ (2^nd ‘𝐵) = (2^nd ‘⟨∪ (1^st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢}⟩)
3		fo1st 6154	. . . . . 6 ⊢ 1^st :V–onto→V
4		fofun 5437	. . . . . 6 ⊢ (1^st :V–onto→V → Fun 1^st )
5	3, 4	ax-mp 5	. . . . 5 ⊢ Fun 1^st
6		npex 7468	. . . . . 6 ⊢ P ∈ V
7	6	ssex 4139	. . . . 5 ⊢ (𝐴 ⊆ P → 𝐴 ∈ V)
8		funimaexg 5298	. . . . 5 ⊢ ((Fun 1^st ∧ 𝐴 ∈ V) → (1^st “ 𝐴) ∈ V)
9	5, 7, 8	sylancr 414	. . . 4 ⊢ (𝐴 ⊆ P → (1^st “ 𝐴) ∈ V)
10		uniexg 4438	. . . 4 ⊢ ((1^st “ 𝐴) ∈ V → ∪ (1^st “ 𝐴) ∈ V)
11	9, 10	syl 14	. . 3 ⊢ (𝐴 ⊆ P → ∪ (1^st “ 𝐴) ∈ V)
12		nqex 7358	. . . 4 ⊢ Q ∈ V
13	12	rabex 4146	. . 3 ⊢ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢} ∈ V
14		op2ndg 6148	. . 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 2222	1 ⊢ (𝐴 ⊆ P → (2^nd ‘𝐵) = {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2^nd “ 𝐴)𝑤 <_Q 𝑢})

Colors of variables: wff set class

Syntax hints: → wi 4 = wceq 1353 ∈ wcel 2148 ∃wrex 2456 {crab 2459 Vcvv 2737 ⊆ wss 3129 ⟨cop 3595 ∪ cuni 3809 ∩ cint 3844 class class class wbr 4002 “ cima 4628 Fun wfun 5208 –onto→wfo 5212 ‘cfv 5214 1^st c1st 6135 2^nd c2nd 6136 Qcnq 7275 <_Q cltq 7280 Pcnp 7286

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4117 ax-sep 4120 ax-pow 4173 ax-pr 4208 ax-un 4432 ax-iinf 4586

This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-reu 2462 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-int 3845 df-iun 3888 df-br 4003 df-opab 4064 df-mpt 4065 df-id 4292 df-iom 4589 df-xp 4631 df-rel 4632 df-cnv 4633 df-co 4634 df-dm 4635 df-rn 4636 df-res 4637 df-ima 4638 df-iota 5176 df-fun 5216 df-fn 5217 df-f 5218 df-f1 5219 df-fo 5220 df-f1o 5221 df-fv 5222 df-1st 6137 df-2nd 6138 df-qs 6537 df-ni 7299 df-nqqs 7343 df-inp 7461

This theorem is referenced by: suplocexprlemmu 7713 suplocexprlemru 7714 suplocexprlemdisj 7715 suplocexprlemloc 7716 suplocexprlemex 7717 suplocexprlemub 7718

W3C validator