Theorem preimagelt

Description: The preimage of a right-open, unbounded below interval, is the complement of a left-closed unbounded above interval. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	preimagelt.x	⊢ Ⅎ 𝑥 𝜑
	preimagelt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
	preimagelt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
Assertion	preimagelt	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } )

Proof

Step	Hyp	Ref	Expression
1		preimagelt.x	⊢ Ⅎ 𝑥 𝜑
2		preimagelt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3		preimagelt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
4		nfcv	⊢ Ⅎ 𝑥 𝐴
5		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 }
6	4 5	nfdif	⊢ Ⅎ 𝑥 ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } )
7		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 }
8		eldifi	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) → 𝑥 ∈ 𝐴 )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ) → 𝑥 ∈ 𝐴 )
10		eldifn	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) → ¬ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } )
11	8	anim1i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ∧ 𝐶 ≤ 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝐵 ) )
12		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝐵 ) )
13	11 12	sylibr	⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ∧ 𝐶 ≤ 𝐵 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } )
14	10 13	mtand	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) → ¬ 𝐶 ≤ 𝐵 )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ) → ¬ 𝐶 ≤ 𝐵 )
16	8 2	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ) → 𝐵 ∈ ℝ* )
17	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ) → 𝐶 ∈ ℝ* )
18	16 17	xrltnled	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ) → ( 𝐵 < 𝐶 ↔ ¬ 𝐶 ≤ 𝐵 ) )
19	15 18	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ) → 𝐵 < 𝐶 )
20		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) )
21	9 19 20	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } )
22		rabidim1	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } → 𝑥 ∈ 𝐴 )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ) → 𝑥 ∈ 𝐴 )
24		rabidim2	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } → 𝐵 < 𝐶 )
25	24	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ) → 𝐵 < 𝐶 )
26	22 2	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ) → 𝐵 ∈ ℝ* )
27	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ) → 𝐶 ∈ ℝ* )
28	26 27	xrltnled	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ) → ( 𝐵 < 𝐶 ↔ ¬ 𝐶 ≤ 𝐵 ) )
29	25 28	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ) → ¬ 𝐶 ≤ 𝐵 )
30	29	intnand	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ) → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝐵 ) )
31	30 12	sylnibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ) → ¬ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } )
32	23 31	eldifd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ) → 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) )
33	21 32	impbida	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) ↔ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ) )
34	1 6 7 33	eqrd	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } )