Theorem preimalegt

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

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

Proof

Step	Hyp	Ref	Expression
1		preimalegt.x	⊢ Ⅎ 𝑥 𝜑
2		preimalegt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3		preimalegt.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	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } ) ) → 𝐶 ∈ ℝ* )
17	8 2	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } ) ) → 𝐵 ∈ ℝ* )
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	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) → 𝐶 ∈ ℝ* )
27	22 2	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) → 𝐵 ∈ ℝ* )
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	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } ) = { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } )