Theorem 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	⊢ Ⅎ 𝑥 𝜑
	pimxrneun.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
	pimxrneun.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ* )
Assertion	pimxrneun	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		pimxrneun.1	⊢ Ⅎ 𝑥 𝜑
2		pimxrneun.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3		pimxrneun.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ* )
4		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 }
5		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 }
6	4 5	nfun	⊢ Ⅎ 𝑥 ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } )
7		simpl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) → 𝑥 ∈ 𝐴 )
8		simpr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) → 𝐵 < 𝐶 )
9	7 8	jca	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) )
10		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) )
11	9 10	sylibr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } )
12	11	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } )
13		elun1	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
14	12 13	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
15	14	3adantl3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐵 < 𝐶 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
16		3simpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) → ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
17	16	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
18	3	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ∈ ℝ* )
19	18	3adantl3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ∈ ℝ* )
20	2	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐵 ∈ ℝ* )
21	20	3adantl3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐵 ∈ ℝ* )
22		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → ¬ 𝐵 < 𝐶 )
23	19 21 22	xrnltled	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ≤ 𝐵 )
24		necom	⊢ ( 𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵 )
25	24	biimpi	⊢ ( 𝐵 ≠ 𝐶 → 𝐶 ≠ 𝐵 )
26	25	adantr	⊢ ( ( 𝐵 ≠ 𝐶 ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ≠ 𝐵 )
27	26	3ad2antl3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ≠ 𝐵 )
28	19 21 23 27	xrleneltd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 < 𝐵 )
29		id	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) )
30	29	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) )
31		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) )
32	30 31	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } )
33		elun2	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
34	32 33	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
35	17 28 34	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
36	15 35	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
37	1 6 36	rabssd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } ⊆ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
38	2	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐵 ∈ ℝ* )
39	3	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐶 ∈ ℝ* )
40		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐵 < 𝐶 )
41	38 39 40	xrltned	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐵 ≠ 𝐶 )
42	41	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 < 𝐶 → 𝐵 ≠ 𝐶 ) )
43	1 42	ss2rabdf	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } )
44	3	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐶 ∈ ℝ* )
45	2	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐵 ∈ ℝ* )
46		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐶 < 𝐵 )
47	44 45 46	xrgtned	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐵 ≠ 𝐶 )
48	47	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 < 𝐵 → 𝐵 ≠ 𝐶 ) )
49	1 48	ss2rabdf	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } )
50	43 49	unssd	⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } )
51	37 50	eqssd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )