Metamath Proof Explorer

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 ⊢Ⅎxφ
preimalegt.b ⊢φ∧x∈A→B∈ℝ*
preimalegt.c ⊢φ→C∈ℝ*
Assertion preimalegt ⊢φ→A∖x∈A|B≤C=x∈A|C<B

Proof

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