Step |
Hyp |
Ref |
Expression |
1 |
|
sate0 |
|- ( U e. ( Fmla ` _om ) -> ( (/) SatE U ) = ( ( ( (/) Sat (/) ) ` _om ) ` U ) ) |
2 |
|
peano1 |
|- (/) e. _om |
3 |
2
|
n0ii |
|- -. _om = (/) |
4 |
3
|
intnan |
|- -. ( x = (/) /\ _om = (/) ) |
5 |
4
|
a1i |
|- ( U e. ( Fmla ` _om ) -> -. ( x = (/) /\ _om = (/) ) ) |
6 |
|
f00 |
|- ( x : _om --> (/) <-> ( x = (/) /\ _om = (/) ) ) |
7 |
5 6
|
sylnibr |
|- ( U e. ( Fmla ` _om ) -> -. x : _om --> (/) ) |
8 |
|
0ex |
|- (/) e. _V |
9 |
8 8
|
pm3.2i |
|- ( (/) e. _V /\ (/) e. _V ) |
10 |
|
satfvel |
|- ( ( ( (/) e. _V /\ (/) e. _V ) /\ U e. ( Fmla ` _om ) /\ x e. ( ( ( (/) Sat (/) ) ` _om ) ` U ) ) -> x : _om --> (/) ) |
11 |
9 10
|
mp3an1 |
|- ( ( U e. ( Fmla ` _om ) /\ x e. ( ( ( (/) Sat (/) ) ` _om ) ` U ) ) -> x : _om --> (/) ) |
12 |
7 11
|
mtand |
|- ( U e. ( Fmla ` _om ) -> -. x e. ( ( ( (/) Sat (/) ) ` _om ) ` U ) ) |
13 |
12
|
alrimiv |
|- ( U e. ( Fmla ` _om ) -> A. x -. x e. ( ( ( (/) Sat (/) ) ` _om ) ` U ) ) |
14 |
|
eq0 |
|- ( ( ( ( (/) Sat (/) ) ` _om ) ` U ) = (/) <-> A. x -. x e. ( ( ( (/) Sat (/) ) ` _om ) ` U ) ) |
15 |
13 14
|
sylibr |
|- ( U e. ( Fmla ` _om ) -> ( ( ( (/) Sat (/) ) ` _om ) ` U ) = (/) ) |
16 |
1 15
|
eqtrd |
|- ( U e. ( Fmla ` _om ) -> ( (/) SatE U ) = (/) ) |
17 |
|
prv |
|- ( ( (/) e. _V /\ U e. ( Fmla ` _om ) ) -> ( (/) |= U <-> ( (/) SatE U ) = ( (/) ^m _om ) ) ) |
18 |
8 17
|
mpan |
|- ( U e. ( Fmla ` _om ) -> ( (/) |= U <-> ( (/) SatE U ) = ( (/) ^m _om ) ) ) |
19 |
2
|
ne0ii |
|- _om =/= (/) |
20 |
|
map0b |
|- ( _om =/= (/) -> ( (/) ^m _om ) = (/) ) |
21 |
19 20
|
mp1i |
|- ( U e. ( Fmla ` _om ) -> ( (/) ^m _om ) = (/) ) |
22 |
21
|
eqeq2d |
|- ( U e. ( Fmla ` _om ) -> ( ( (/) SatE U ) = ( (/) ^m _om ) <-> ( (/) SatE U ) = (/) ) ) |
23 |
18 22
|
bitrd |
|- ( U e. ( Fmla ` _om ) -> ( (/) |= U <-> ( (/) SatE U ) = (/) ) ) |
24 |
16 23
|
mpbird |
|- ( U e. ( Fmla ` _om ) -> (/) |= U ) |