iooinsup - Intuitionistic Logic Explorer

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

Theorem iooinsup 11658

Description: Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 22-May-2023.)

**Assertion**
Ref	Expression
iooinsup	⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = (sup({𝐴, 𝐶}, ℝ^, < )(,)inf({𝐵, 𝐷}, ℝ^*, < )))

Proof of Theorem iooinsup Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		inrab 3449	. . 3 ⊢ ({𝑧 ∈ ℝ^* ∣ (𝐴 < 𝑧 ∧ 𝑧 < 𝐵)} ∩ {𝑧 ∈ ℝ^* ∣ (𝐶 < 𝑧 ∧ 𝑧 < 𝐷)}) = {𝑧 ∈ ℝ^* ∣ ((𝐴 < 𝑧 ∧ 𝑧 < 𝐵) ∧ (𝐶 < 𝑧 ∧ 𝑧 < 𝐷))}
2		iooval 10045	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐴(,)𝐵) = {𝑧 ∈ ℝ^ ∣ (𝐴 < 𝑧 ∧ 𝑧 < 𝐵)})
3		iooval 10045	. . . 4 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^) → (𝐶(,)𝐷) = {𝑧 ∈ ℝ^ ∣ (𝐶 < 𝑧 ∧ 𝑧 < 𝐷)})
4	2, 3	ineqan12d 3380	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = ({𝑧 ∈ ℝ^ ∣ (𝐴 < 𝑧 ∧ 𝑧 < 𝐵)} ∩ {𝑧 ∈ ℝ^* ∣ (𝐶 < 𝑧 ∧ 𝑧 < 𝐷)}))
5		xrmaxltsup 11639	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) → (sup({𝐴, 𝐶}, ℝ^, < ) < 𝑧 ↔ (𝐴 < 𝑧 ∧ 𝐶 < 𝑧)))
6	5	ad4ant124 1219	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^) ∧ (𝐵 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) ∧ 𝑧 ∈ ℝ^) → (sup({𝐴, 𝐶}, ℝ^*, < ) < 𝑧 ↔ (𝐴 < 𝑧 ∧ 𝐶 < 𝑧)))
7		xrltmininf 11651	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^) → (𝑧 < inf({𝐵, 𝐷}, ℝ^, < ) ↔ (𝑧 < 𝐵 ∧ 𝑧 < 𝐷)))
8	7	3expb 1207	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝐵 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^)) → (𝑧 < inf({𝐵, 𝐷}, ℝ^, < ) ↔ (𝑧 < 𝐵 ∧ 𝑧 < 𝐷)))
9	8	ancoms 268	. . . . . . . 8 ⊢ (((𝐵 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^) ∧ 𝑧 ∈ ℝ^) → (𝑧 < inf({𝐵, 𝐷}, ℝ^*, < ) ↔ (𝑧 < 𝐵 ∧ 𝑧 < 𝐷)))
10	9	adantll 476	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^) ∧ (𝐵 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) ∧ 𝑧 ∈ ℝ^) → (𝑧 < inf({𝐵, 𝐷}, ℝ^*, < ) ↔ (𝑧 < 𝐵 ∧ 𝑧 < 𝐷)))
11	6, 10	anbi12d 473	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^) ∧ (𝐵 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) ∧ 𝑧 ∈ ℝ^) → ((sup({𝐴, 𝐶}, ℝ^, < ) < 𝑧 ∧ 𝑧 < inf({𝐵, 𝐷}, ℝ^, < )) ↔ ((𝐴 < 𝑧 ∧ 𝐶 < 𝑧) ∧ (𝑧 < 𝐵 ∧ 𝑧 < 𝐷))))
12		an4 586	. . . . . 6 ⊢ (((𝐴 < 𝑧 ∧ 𝑧 < 𝐵) ∧ (𝐶 < 𝑧 ∧ 𝑧 < 𝐷)) ↔ ((𝐴 < 𝑧 ∧ 𝐶 < 𝑧) ∧ (𝑧 < 𝐵 ∧ 𝑧 < 𝐷)))
13	11, 12	bitr4di 198	. . . . 5 ⊢ ((((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^) ∧ (𝐵 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) ∧ 𝑧 ∈ ℝ^) → ((sup({𝐴, 𝐶}, ℝ^, < ) < 𝑧 ∧ 𝑧 < inf({𝐵, 𝐷}, ℝ^, < )) ↔ ((𝐴 < 𝑧 ∧ 𝑧 < 𝐵) ∧ (𝐶 < 𝑧 ∧ 𝑧 < 𝐷))))
14	13	rabbidva 2761	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^) ∧ (𝐵 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) → {𝑧 ∈ ℝ^ ∣ (sup({𝐴, 𝐶}, ℝ^, < ) < 𝑧 ∧ 𝑧 < inf({𝐵, 𝐷}, ℝ^, < ))} = {𝑧 ∈ ℝ^* ∣ ((𝐴 < 𝑧 ∧ 𝑧 < 𝐵) ∧ (𝐶 < 𝑧 ∧ 𝑧 < 𝐷))})
15	14	an4s 588	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) → {𝑧 ∈ ℝ^ ∣ (sup({𝐴, 𝐶}, ℝ^, < ) < 𝑧 ∧ 𝑧 < inf({𝐵, 𝐷}, ℝ^, < ))} = {𝑧 ∈ ℝ^* ∣ ((𝐴 < 𝑧 ∧ 𝑧 < 𝐵) ∧ (𝐶 < 𝑧 ∧ 𝑧 < 𝐷))})
16	1, 4, 15	3eqtr4a 2265	. 2 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = {𝑧 ∈ ℝ^ ∣ (sup({𝐴, 𝐶}, ℝ^, < ) < 𝑧 ∧ 𝑧 < inf({𝐵, 𝐷}, ℝ^, < ))})
17		xrmaxcl 11633	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^) → sup({𝐴, 𝐶}, ℝ^, < ) ∈ ℝ^*)
18		xrmincl 11647	. . . 4 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^) → inf({𝐵, 𝐷}, ℝ^, < ) ∈ ℝ^*)
19		iooval 10045	. . . 4 ⊢ ((sup({𝐴, 𝐶}, ℝ^, < ) ∈ ℝ^ ∧ inf({𝐵, 𝐷}, ℝ^, < ) ∈ ℝ^) → (sup({𝐴, 𝐶}, ℝ^, < )(,)inf({𝐵, 𝐷}, ℝ^, < )) = {𝑧 ∈ ℝ^* ∣ (sup({𝐴, 𝐶}, ℝ^, < ) < 𝑧 ∧ 𝑧 < inf({𝐵, 𝐷}, ℝ^, < ))})
20	17, 18, 19	syl2an 289	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^) ∧ (𝐵 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) → (sup({𝐴, 𝐶}, ℝ^, < )(,)inf({𝐵, 𝐷}, ℝ^, < )) = {𝑧 ∈ ℝ^ ∣ (sup({𝐴, 𝐶}, ℝ^, < ) < 𝑧 ∧ 𝑧 < inf({𝐵, 𝐷}, ℝ^, < ))})
21	20	an4s 588	. 2 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) → (sup({𝐴, 𝐶}, ℝ^, < )(,)inf({𝐵, 𝐷}, ℝ^, < )) = {𝑧 ∈ ℝ^ ∣ (sup({𝐴, 𝐶}, ℝ^, < ) < 𝑧 ∧ 𝑧 < inf({𝐵, 𝐷}, ℝ^, < ))})
22	16, 21	eqtr4d 2242	1 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐷 ∈ ℝ^)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = (sup({𝐴, 𝐶}, ℝ^, < )(,)inf({𝐵, 𝐷}, ℝ^*, < )))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1373 ∈ wcel 2177 {crab 2489 ∩ cin 3169 {cpr 3638 class class class wbr 4050 (class class class)co 5956 supcsup 7098 infcinf 7099 ℝ^*cxr 8121 < clt 8122 (,)cioo 10025

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4166 ax-sep 4169 ax-nul 4177 ax-pow 4225 ax-pr 4260 ax-un 4487 ax-setind 4592 ax-iinf 4643 ax-cnex 8031 ax-resscn 8032 ax-1cn 8033 ax-1re 8034 ax-icn 8035 ax-addcl 8036 ax-addrcl 8037 ax-mulcl 8038 ax-mulrcl 8039 ax-addcom 8040 ax-mulcom 8041 ax-addass 8042 ax-mulass 8043 ax-distr 8044 ax-i2m1 8045 ax-0lt1 8046 ax-1rid 8047 ax-0id 8048 ax-rnegex 8049 ax-precex 8050 ax-cnre 8051 ax-pre-ltirr 8052 ax-pre-ltwlin 8053 ax-pre-lttrn 8054 ax-pre-apti 8055 ax-pre-ltadd 8056 ax-pre-mulgt0 8057 ax-pre-mulext 8058 ax-arch 8059 ax-caucvg 8060

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-if 3576 df-pw 3622 df-sn 3643 df-pr 3644 df-op 3646 df-uni 3856 df-int 3891 df-iun 3934 df-br 4051 df-opab 4113 df-mpt 4114 df-tr 4150 df-id 4347 df-po 4350 df-iso 4351 df-iord 4420 df-on 4422 df-ilim 4423 df-suc 4425 df-iom 4646 df-xp 4688 df-rel 4689 df-cnv 4690 df-co 4691 df-dm 4692 df-rn 4693 df-res 4694 df-ima 4695 df-iota 5240 df-fun 5281 df-fn 5282 df-f 5283 df-f1 5284 df-fo 5285 df-f1o 5286 df-fv 5287 df-isom 5288 df-riota 5911 df-ov 5959 df-oprab 5960 df-mpo 5961 df-1st 6238 df-2nd 6239 df-recs 6403 df-frec 6489 df-sup 7100 df-inf 7101 df-pnf 8124 df-mnf 8125 df-xr 8126 df-ltxr 8127 df-le 8128 df-sub 8260 df-neg 8261 df-reap 8663 df-ap 8670 df-div 8761 df-inn 9052 df-2 9110 df-3 9111 df-4 9112 df-n0 9311 df-z 9388 df-uz 9664 df-rp 9791 df-xneg 9909 df-ioo 10029 df-seqfrec 10610 df-exp 10701 df-cj 11223 df-re 11224 df-im 11225 df-rsqrt 11379 df-abs 11380

This theorem is referenced by: qtopbasss 15063 tgioo 15096

W3C validator