Step |
Hyp |
Ref |
Expression |
1 |
|
pwexg |
|- ( B e. A -> ~P B e. _V ) |
2 |
|
elpw2g |
|- ( ~P B e. _V -> ( F e. ~P ~P B <-> F C_ ~P B ) ) |
3 |
1 2
|
syl |
|- ( B e. A -> ( F e. ~P ~P B <-> F C_ ~P B ) ) |
4 |
3
|
anbi1d |
|- ( B e. A -> ( ( F e. ~P ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) ) |
5 |
|
elex |
|- ( B e. A -> B e. _V ) |
6 |
5
|
biantrurd |
|- ( B e. A -> ( ( F e. ~P ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) <-> ( B e. _V /\ ( F e. ~P ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) ) ) |
7 |
4 6
|
bitr3d |
|- ( B e. A -> ( ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) <-> ( B e. _V /\ ( F e. ~P ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) ) ) |
8 |
|
df-fbas |
|- fBas = ( z e. _V |-> { w e. ~P ~P z | ( w =/= (/) /\ (/) e/ w /\ A. x e. w A. y e. w ( w i^i ~P ( x i^i y ) ) =/= (/) ) } ) |
9 |
|
neeq1 |
|- ( w = F -> ( w =/= (/) <-> F =/= (/) ) ) |
10 |
|
neleq2 |
|- ( w = F -> ( (/) e/ w <-> (/) e/ F ) ) |
11 |
|
ineq1 |
|- ( w = F -> ( w i^i ~P ( x i^i y ) ) = ( F i^i ~P ( x i^i y ) ) ) |
12 |
11
|
neeq1d |
|- ( w = F -> ( ( w i^i ~P ( x i^i y ) ) =/= (/) <-> ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) |
13 |
12
|
raleqbi1dv |
|- ( w = F -> ( A. y e. w ( w i^i ~P ( x i^i y ) ) =/= (/) <-> A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) |
14 |
13
|
raleqbi1dv |
|- ( w = F -> ( A. x e. w A. y e. w ( w i^i ~P ( x i^i y ) ) =/= (/) <-> A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) |
15 |
9 10 14
|
3anbi123d |
|- ( w = F -> ( ( w =/= (/) /\ (/) e/ w /\ A. x e. w A. y e. w ( w i^i ~P ( x i^i y ) ) =/= (/) ) <-> ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) |
16 |
15
|
adantl |
|- ( ( z = B /\ w = F ) -> ( ( w =/= (/) /\ (/) e/ w /\ A. x e. w A. y e. w ( w i^i ~P ( x i^i y ) ) =/= (/) ) <-> ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) |
17 |
|
pweq |
|- ( z = B -> ~P z = ~P B ) |
18 |
17
|
pweqd |
|- ( z = B -> ~P ~P z = ~P ~P B ) |
19 |
|
vpwex |
|- ~P z e. _V |
20 |
19
|
pwex |
|- ~P ~P z e. _V |
21 |
20
|
a1i |
|- ( z e. _V -> ~P ~P z e. _V ) |
22 |
8 16 18 21
|
elmptrab |
|- ( F e. ( fBas ` B ) <-> ( B e. _V /\ F e. ~P ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) |
23 |
|
3anass |
|- ( ( B e. _V /\ F e. ~P ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) <-> ( B e. _V /\ ( F e. ~P ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) ) |
24 |
22 23
|
bitri |
|- ( F e. ( fBas ` B ) <-> ( B e. _V /\ ( F e. ~P ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) ) |
25 |
7 24
|
syl6rbbr |
|- ( B e. A -> ( F e. ( fBas ` B ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) ) |