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	birani	⊢ ( ( 𝐵 ≠ 𝐶 ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ≠ 𝐵 )
26	25	3ad2antl3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ≠ 𝐵 )
27	19 21 23 26	xrleneltd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 < 𝐵 )
28		id	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) )
29	28	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) )
30		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) )
31	29 30	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } )
32		elun2	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
33	31 32	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
34	17 27 33	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
35	15 34	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
36	1 6 35	rabssd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } ⊆ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
37	2	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐵 ∈ ℝ* )
38	3	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐶 ∈ ℝ* )
39		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐵 < 𝐶 )
40	37 38 39	xrltned	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐵 ≠ 𝐶 )
41	40	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 < 𝐶 → 𝐵 ≠ 𝐶 ) )
42	1 41	ss2rabdf	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } )
43	3	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐶 ∈ ℝ* )
44	2	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐵 ∈ ℝ* )
45		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐶 < 𝐵 )
46	43 44 45	xrgtned	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐵 ≠ 𝐶 )
47	46	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 < 𝐵 → 𝐵 ≠ 𝐶 ) )
48	1 47	ss2rabdf	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } )
49	42 48	unssd	⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } )
50	36 49	eqssd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )