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	birani	$⊢ (B \neq C \land \neg B < C) \to C \neq B$
26	25	3ad2antl3	$⊢ ((φ \land x \in A \land B \neq C) \land \neg B < C) \to C \neq B$
27	19 21 23 26	xrleneltd	$⊢ ((φ \land x \in A \land B \neq C) \land \neg B < C) \to C < B$
28		id	$⊢ (x \in A \land C < B) \to (x \in A \land C < B)$
29	28	adantll	$⊢ ((φ \land x \in A) \land C < B) \to (x \in A \land C < B)$
30		rabid	$⊢ x \in \{x \in A \| C < B\} \leftrightarrow (x \in A \land C < B)$
31	29 30	sylibr	$⊢ ((φ \land x \in A) \land C < B) \to x \in \{x \in A \| C < B\}$
32		elun2	$⊢ x \in \{x \in A \| C < B\} \to x \in (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
33	31 32	syl	$⊢ ((φ \land x \in A) \land C < B) \to x \in (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
34	17 27 33	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\})$
35	15 34	pm2.61dan	$⊢ (φ \land x \in A \land B \neq C) \to x \in (\{x \in A \| B < C\} \cup \{x \in A \| C < B\})$
36	1 6 35	rabssd	$⊢ φ \to \{x \in A \| B \neq C\} \subseteq \{x \in A \| B < C\} \cup \{x \in A \| C < B\}$
37	2	adantr	$⊢ ((φ \land x \in A) \land B < C) \to B \in ℝ^{*}$
38	3	adantr	$⊢ ((φ \land x \in A) \land B < C) \to C \in ℝ^{*}$
39		simpr	$⊢ ((φ \land x \in A) \land B < C) \to B < C$
40	37 38 39	xrltned	$⊢ ((φ \land x \in A) \land B < C) \to B \neq C$
41	40	ex	$⊢ (φ \land x \in A) \to (B < C \to B \neq C)$
42	1 41	ss2rabdf	$⊢ φ \to \{x \in A \| B < C\} \subseteq \{x \in A \| B \neq C\}$
43	3	adantr	$⊢ ((φ \land x \in A) \land C < B) \to C \in ℝ^{*}$
44	2	adantr	$⊢ ((φ \land x \in A) \land C < B) \to B \in ℝ^{*}$
45		simpr	$⊢ ((φ \land x \in A) \land C < B) \to C < B$
46	43 44 45	xrgtned	$⊢ ((φ \land x \in A) \land C < B) \to B \neq C$
47	46	ex	$⊢ (φ \land x \in A) \to (C < B \to B \neq C)$
48	1 47	ss2rabdf	$⊢ φ \to \{x \in A \| C < B\} \subseteq \{x \in A \| B \neq C\}$
49	42 48	unssd	$⊢ φ \to \{x \in A \| B < C\} \cup \{x \in A \| C < B\} \subseteq \{x \in A \| B \neq C\}$
50	36 49	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