Metamath Proof Explorer

Theorem isfildlem

Description: Lemma for isfild . (Contributed by Mario Carneiro, 1-Dec-2013)

Ref Expression
Hypotheses isfild.1 
|- ( ph -> ( x e. F <-> ( x C_ A /\ ps ) ) )
isfild.2 
|- ( ph -> A e. V )
Assertion isfildlem 
|- ( ph -> ( B e. F <-> ( B C_ A /\ [. B / x ]. ps ) ) )

Proof

Step Hyp Ref Expression
1 isfild.1 
 |-  ( ph -> ( x e. F <-> ( x C_ A /\ ps ) ) )
2 isfild.2 
 |-  ( ph -> A e. V )
3 elex 
 |-  ( B e. F -> B e. _V )
4 3 a1i 
 |-  ( ph -> ( B e. F -> B e. _V ) )
5 ssexg 
 |-  ( ( B C_ A /\ A e. V ) -> B e. _V )
6 5 expcom 
 |-  ( A e. V -> ( B C_ A -> B e. _V ) )
7 2 6 syl 
 |-  ( ph -> ( B C_ A -> B e. _V ) )
8 7 adantrd 
 |-  ( ph -> ( ( B C_ A /\ [. B / x ]. ps ) -> B e. _V ) )
9 eleq1 
 |-  ( y = B -> ( y e. F <-> B e. F ) )
10 sseq1 
 |-  ( y = B -> ( y C_ A <-> B C_ A ) )
11 dfsbcq 
 |-  ( y = B -> ( [. y / x ]. ps <-> [. B / x ]. ps ) )
12 10 11 anbi12d 
 |-  ( y = B -> ( ( y C_ A /\ [. y / x ]. ps ) <-> ( B C_ A /\ [. B / x ]. ps ) ) )
13 9 12 bibi12d 
 |-  ( y = B -> ( ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) ) <-> ( B e. F <-> ( B C_ A /\ [. B / x ]. ps ) ) ) )
14 13 imbi2d 
 |-  ( y = B -> ( ( ph -> ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) ) ) <-> ( ph -> ( B e. F <-> ( B C_ A /\ [. B / x ]. ps ) ) ) ) )
15 nfv 
 |-  F/ x ph
16 nfv 
 |-  F/ x y e. F
17 nfv 
 |-  F/ x y C_ A
18 nfsbc1v 
 |-  F/ x [. y / x ]. ps
19 17 18 nfan 
 |-  F/ x ( y C_ A /\ [. y / x ]. ps )
20 16 19 nfbi 
 |-  F/ x ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) )
21 15 20 nfim 
 |-  F/ x ( ph -> ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) ) )
22 eleq1 
 |-  ( x = y -> ( x e. F <-> y e. F ) )
23 sseq1 
 |-  ( x = y -> ( x C_ A <-> y C_ A ) )
24 sbceq1a 
 |-  ( x = y -> ( ps <-> [. y / x ]. ps ) )
25 23 24 anbi12d 
 |-  ( x = y -> ( ( x C_ A /\ ps ) <-> ( y C_ A /\ [. y / x ]. ps ) ) )
26 22 25 bibi12d 
 |-  ( x = y -> ( ( x e. F <-> ( x C_ A /\ ps ) ) <-> ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) ) ) )
27 26 imbi2d 
 |-  ( x = y -> ( ( ph -> ( x e. F <-> ( x C_ A /\ ps ) ) ) <-> ( ph -> ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) ) ) ) )
28 21 27 1 chvarfv 
 |-  ( ph -> ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) ) )
29 14 28 vtoclg 
 |-  ( B e. _V -> ( ph -> ( B e. F <-> ( B C_ A /\ [. B / x ]. ps ) ) ) )
30 29 com12 
 |-  ( ph -> ( B e. _V -> ( B e. F <-> ( B C_ A /\ [. B / x ]. ps ) ) ) )
31 4 8 30 pm5.21ndd 
 |-  ( ph -> ( B e. F <-> ( B C_ A /\ [. B / x ]. ps ) ) )