Metamath Proof Explorer

Theorem hstrlem5

Description: Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hstrlem3.1 ⊢S=x∈Cℋ⟼projℎ⁡x⁡u
hstrlem3.2 ⊢φ↔u∈A∖B∧normℎ⁡u=1
hstrlem3.3 ⊢A∈Cℋ
hstrlem3.4 ⊢B∈Cℋ
Assertion hstrlem5 ⊢φ→normℎ⁡S⁡B<1

Proof

Step Hyp Ref Expression
1 hstrlem3.1 ⊢S=x∈Cℋ⟼projℎ⁡x⁡u
2 hstrlem3.2 ⊢φ↔u∈A∖B∧normℎ⁡u=1
3 hstrlem3.3 ⊢A∈Cℋ
4 hstrlem3.4 ⊢B∈Cℋ
5 1 hstrlem2 ⊢B∈Cℋ→S⁡B=projℎ⁡B⁡u
6 5 fveq2d ⊢B∈Cℋ→normℎ⁡S⁡B=normℎ⁡projℎ⁡B⁡u
7 4 6 ax-mp ⊢normℎ⁡S⁡B=normℎ⁡projℎ⁡B⁡u
8 eldif ⊢u∈A∖B↔u∈A∧¬u∈B
9 3 cheli ⊢u∈A→u∈ℋ
10 pjnel ⊢B∈Cℋ∧u∈ℋ→¬u∈B↔normℎ⁡projℎ⁡B⁡u<normℎ⁡u
11 4 10 mpan ⊢u∈ℋ→¬u∈B↔normℎ⁡projℎ⁡B⁡u<normℎ⁡u
12 11 biimpa ⊢u∈ℋ∧¬u∈B→normℎ⁡projℎ⁡B⁡u<normℎ⁡u
13 9 12 sylan ⊢u∈A∧¬u∈B→normℎ⁡projℎ⁡B⁡u<normℎ⁡u
14 8 13 sylbi ⊢u∈A∖B→normℎ⁡projℎ⁡B⁡u<normℎ⁡u
15 breq2 ⊢normℎ⁡u=1→normℎ⁡projℎ⁡B⁡u<normℎ⁡u↔normℎ⁡projℎ⁡B⁡u<1
16 14 15 imbitrid ⊢normℎ⁡u=1→u∈A∖B→normℎ⁡projℎ⁡B⁡u<1
17 16 impcom ⊢u∈A∖B∧normℎ⁡u=1→normℎ⁡projℎ⁡B⁡u<1
18 7 17 eqbrtrid ⊢u∈A∖B∧normℎ⁡u=1→normℎ⁡S⁡B<1
19 2 18 sylbi ⊢φ→normℎ⁡S⁡B<1