pimxrneun

Description: The preimage of a set of extended reals that does not contain a value C is the union of the preimage of the elements smaller than C and the preimage of the subset of elements larger than C . (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	pimxrneun.1	$⊢ Ⅎ x φ$
	pimxrneun.2	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
	pimxrneun.3	$⊢ (φ \land x \in A) \to C \in ℝ^{*}$
Assertion	pimxrneun	$⊢ φ \to \{x \in A \| B \neq C\} = \{x \in A \| B < C\} \cup \{x \in A \| C < B\}$

Proof

Step	Hyp	Ref	Expression
1		pimxrneun.1	$⊢ Ⅎ x φ$
2		pimxrneun.2	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
3		pimxrneun.3	$⊢ (φ \land x \in A) \to C \in ℝ^{*}$
4		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| B < C\}$
5		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| C < B\}$
6	4 5	nfun	$⊢ \underline{Ⅎ} x (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
7		simpl	$⊢ (x \in A \land B < C) \to x \in A$
8		simpr	$⊢ (x \in A \land B < C) \to B < C$
9	7 8	jca	$⊢ (x \in A \land B < C) \to (x \in A \land B < C)$
10		rabid	$⊢ x \in \{x \in A \| B < C\} \leftrightarrow (x \in A \land B < C)$
11	9 10	sylibr	$⊢ (x \in A \land B < C) \to x \in \{x \in A \| B < C\}$
12	11	adantll	$⊢ ((φ \land x \in A) \land B < C) \to x \in \{x \in A \| B < C\}$
13		elun1	$⊢ x \in \{x \in A \| B < C\} \to x \in (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
14	12 13	syl	$⊢ ((φ \land x \in A) \land B < C) \to x \in (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
15	14	3adantl3	$⊢ ((φ \land x \in A \land B \neq C) \land B < C) \to x \in (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
16		3simpa	$⊢ (φ \land x \in A \land B \neq C) \to (φ \land x \in A)$
17	16	adantr	$⊢ ((φ \land x \in A \land B \neq C) \land \neg B < C) \to (φ \land x \in A)$
18	3	adantr	$⊢ ((φ \land x \in A) \land \neg B < C) \to C \in ℝ^{*}$
19	18	3adantl3	$⊢ ((φ \land x \in A \land B \neq C) \land \neg B < C) \to C \in ℝ^{*}$
20	2	adantr	$⊢ ((φ \land x \in A) \land \neg B < C) \to B \in ℝ^{*}$
21	20	3adantl3	$⊢ ((φ \land x \in A \land B \neq C) \land \neg B < C) \to B \in ℝ^{*}$
22		simpr	$⊢ ((φ \land x \in A \land B \neq C) \land \neg B < C) \to \neg B < C$
23	19 21 22	xrnltled	$⊢ ((φ \land x \in A \land B \neq C) \land \neg B < C) \to C \leq B$
24		necom	$⊢ B \neq C \leftrightarrow C \neq B$
25	24	biimpi	$⊢ B \neq C \to C \neq B$
26	25	adantr	$⊢ (B \neq C \land \neg B < C) \to C \neq B$
27	26	3ad2antl3	$⊢ ((φ \land x \in A \land B \neq C) \land \neg B < C) \to C \neq B$
28	19 21 23 27	xrleneltd	$⊢ ((φ \land x \in A \land B \neq C) \land \neg B < C) \to C < B$
29		id	$⊢ (x \in A \land C < B) \to (x \in A \land C < B)$
30	29	adantll	$⊢ ((φ \land x \in A) \land C < B) \to (x \in A \land C < B)$
31		rabid	$⊢ x \in \{x \in A \| C < B\} \leftrightarrow (x \in A \land C < B)$
32	30 31	sylibr	$⊢ ((φ \land x \in A) \land C < B) \to x \in \{x \in A \| C < B\}$
33		elun2	$⊢ x \in \{x \in A \| C < B\} \to x \in (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
34	32 33	syl	$⊢ ((φ \land x \in A) \land C < B) \to x \in (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
35	17 28 34	syl2anc	$⊢ ((φ \land x \in A \land B \neq C) \land \neg B < C) \to x \in (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
36	15 35	pm2.61dan	$⊢ (φ \land x \in A \land B \neq C) \to x \in (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
37	1 6 36	rabssd	$⊢ φ \to \{x \in A \| B \neq C\} \subseteq \{x \in A \| B < C\} \cup \{x \in A \| C < B\}$
38	2	adantr	$⊢ ((φ \land x \in A) \land B < C) \to B \in ℝ^{*}$
39	3	adantr	$⊢ ((φ \land x \in A) \land B < C) \to C \in ℝ^{*}$
40		simpr	$⊢ ((φ \land x \in A) \land B < C) \to B < C$
41	38 39 40	xrltned	$⊢ ((φ \land x \in A) \land B < C) \to B \neq C$
42	41	ex	$⊢ (φ \land x \in A) \to (B < C \to B \neq C)$
43	1 42	ss2rabdf	$⊢ φ \to \{x \in A \| B < C\} \subseteq \{x \in A \| B \neq C\}$
44	3	adantr	$⊢ ((φ \land x \in A) \land C < B) \to C \in ℝ^{*}$
45	2	adantr	$⊢ ((φ \land x \in A) \land C < B) \to B \in ℝ^{*}$
46		simpr	$⊢ ((φ \land x \in A) \land C < B) \to C < B$
47	44 45 46	xrgtned	$⊢ ((φ \land x \in A) \land C < B) \to B \neq C$
48	47	ex	$⊢ (φ \land x \in A) \to (C < B \to B \neq C)$
49	1 48	ss2rabdf	$⊢ φ \to \{x \in A \| C < B\} \subseteq \{x \in A \| B \neq C\}$
50	43 49	unssd	$⊢ φ \to \{x \in A \| B < C\} \cup \{x \in A \| C < B\} \subseteq \{x \in A \| B \neq C\}$
51	37 50	eqssd	$⊢ φ \to \{x \in A \| B \neq C\} = \{x \in A \| B < C\} \cup \{x \in A \| C < B\}$

Metamath Proof Explorer

Theorem pimxrneun

Proof