Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem58 Structured version   Unicode version

Theorem stoweidlem58 27774
 Description: This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem58.1
stoweidlem58.2
stoweidlem58.3
stoweidlem58.4
stoweidlem58.5
stoweidlem58.6
stoweidlem58.7
stoweidlem58.8
stoweidlem58.9
stoweidlem58.10
stoweidlem58.11
stoweidlem58.12
stoweidlem58.13
stoweidlem58.14
stoweidlem58.15
stoweidlem58.16
stoweidlem58.17
stoweidlem58.18
Assertion
Ref Expression
stoweidlem58
Distinct variable groups:   ,,,,,   ,,,   ,,,,   ,,,   ,,,   ,,,,   ,,,,   ,,,,   ,,,   ,,,,   ,,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,)   (,,)   (,,,,,,)   ()   (,)   (,)   (,,)   (,,,,,)

Proof of Theorem stoweidlem58
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem58.1 . . 3
2 stoweidlem58.3 . . . 4
31nfeq1 2580 . . . 4
42, 3nfan 1846 . . 3
5 eqid 2435 . . 3
6 stoweidlem58.5 . . 3
7 stoweidlem58.11 . . . 4
9 stoweidlem58.13 . . . 4
11 stoweidlem58.17 . . . 4
13 simpr 448 . . 3
141, 4, 5, 6, 8, 10, 12, 13stoweidlem18 27734 . 2
15 stoweidlem58.2 . . 3
16 nfcv 2571 . . . . 5
171, 16nfne 2689 . . . 4
182, 17nfan 1846 . . 3
19 eqid 2435 . . 3
20 eqid 2435 . . 3
21 stoweidlem58.4 . . 3
22 stoweidlem58.6 . . 3
23 stoweidlem58.16 . . 3
24 stoweidlem58.7 . . . 4
26 stoweidlem58.8 . . . 4
28 stoweidlem58.9 . . . 4
30 stoweidlem58.10 . . . 4
33 stoweidlem58.12 . . . 4