Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Godel-sets of formulas - part 1
satfv1lem
Next ⟩
satfv1
Metamath Proof Explorer
Ascii
Unicode
Theorem
satfv1lem
Description:
Lemma for
satfv1
.
(Contributed by
AV
, 9-Nov-2023)
Ref
Expression
Assertion
satfv1lem
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
→
a
∈
M
ω
|
∀
z
∈
M
N
z
∪
a
↾
ω
∖
N
∈
b
∈
M
ω
|
b
I
E
b
J
=
a
∈
M
ω
|
∀
z
∈
M
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
Proof
Step
Hyp
Ref
Expression
1
fveq1
ω
ω
⊢
b
=
N
z
∪
a
↾
ω
∖
N
→
b
I
=
N
z
∪
a
↾
ω
∖
N
I
2
fveq1
ω
ω
⊢
b
=
N
z
∪
a
↾
ω
∖
N
→
b
J
=
N
z
∪
a
↾
ω
∖
N
J
3
1
2
breq12d
ω
ω
ω
⊢
b
=
N
z
∪
a
↾
ω
∖
N
→
b
I
E
b
J
↔
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
4
3
elrab
ω
ω
ω
ω
ω
ω
⊢
N
z
∪
a
↾
ω
∖
N
∈
b
∈
M
ω
|
b
I
E
b
J
↔
N
z
∪
a
↾
ω
∖
N
∈
M
ω
∧
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
5
4
a1i
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
z
∪
a
↾
ω
∖
N
∈
b
∈
M
ω
|
b
I
E
b
J
↔
N
z
∪
a
↾
ω
∖
N
∈
M
ω
∧
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
6
elex
ω
⊢
N
∈
ω
→
N
∈
V
7
6
3ad2ant1
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
→
N
∈
V
8
7
ad2antrr
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
∈
V
9
simpr
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
z
∈
M
10
8
9
fsnd
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
z
:
N
⟶
M
11
elmapex
ω
ω
⊢
a
∈
M
ω
→
M
∈
V
∧
ω
∈
V
12
11
simpld
ω
⊢
a
∈
M
ω
→
M
∈
V
13
12
adantr
ω
⊢
a
∈
M
ω
∧
z
∈
M
→
M
∈
V
14
snex
⊢
N
∈
V
15
14
a1i
ω
⊢
a
∈
M
ω
∧
z
∈
M
→
N
∈
V
16
13
15
elmapd
ω
⊢
a
∈
M
ω
∧
z
∈
M
→
N
z
∈
M
N
↔
N
z
:
N
⟶
M
17
16
adantll
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
z
∈
M
N
↔
N
z
:
N
⟶
M
18
10
17
mpbird
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
z
∈
M
N
19
elmapi
ω
ω
⊢
a
∈
M
ω
→
a
:
ω
⟶
M
20
difssd
ω
ω
ω
⊢
a
∈
M
ω
→
ω
∖
N
⊆
ω
21
19
20
fssresd
ω
ω
ω
⊢
a
∈
M
ω
→
a
↾
ω
∖
N
:
ω
∖
N
⟶
M
22
omex
ω
⊢
ω
∈
V
23
22
difexi
ω
⊢
ω
∖
N
∈
V
24
23
a1i
ω
ω
⊢
a
∈
M
ω
→
ω
∖
N
∈
V
25
12
24
elmapd
ω
ω
ω
ω
ω
⊢
a
∈
M
ω
→
a
↾
ω
∖
N
∈
M
ω
∖
N
↔
a
↾
ω
∖
N
:
ω
∖
N
⟶
M
26
21
25
mpbird
ω
ω
ω
⊢
a
∈
M
ω
→
a
↾
ω
∖
N
∈
M
ω
∖
N
27
26
adantl
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
→
a
↾
ω
∖
N
∈
M
ω
∖
N
28
27
adantr
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
a
↾
ω
∖
N
∈
M
ω
∖
N
29
res0
⊢
N
z
↾
∅
=
∅
30
res0
ω
⊢
a
↾
ω
∖
N
↾
∅
=
∅
31
29
30
eqtr4i
ω
⊢
N
z
↾
∅
=
a
↾
ω
∖
N
↾
∅
32
disjdif
ω
⊢
N
∩
ω
∖
N
=
∅
33
32
reseq2i
ω
⊢
N
z
↾
N
∩
ω
∖
N
=
N
z
↾
∅
34
32
reseq2i
ω
ω
ω
⊢
a
↾
ω
∖
N
↾
N
∩
ω
∖
N
=
a
↾
ω
∖
N
↾
∅
35
31
33
34
3eqtr4i
ω
ω
ω
⊢
N
z
↾
N
∩
ω
∖
N
=
a
↾
ω
∖
N
↾
N
∩
ω
∖
N
36
35
a1i
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
z
↾
N
∩
ω
∖
N
=
a
↾
ω
∖
N
↾
N
∩
ω
∖
N
37
elmapresaun
ω
ω
ω
ω
ω
ω
ω
⊢
N
z
∈
M
N
∧
a
↾
ω
∖
N
∈
M
ω
∖
N
∧
N
z
↾
N
∩
ω
∖
N
=
a
↾
ω
∖
N
↾
N
∩
ω
∖
N
→
N
z
∪
a
↾
ω
∖
N
∈
M
N
∪
ω
∖
N
38
18
28
36
37
syl3anc
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
z
∪
a
↾
ω
∖
N
∈
M
N
∪
ω
∖
N
39
uncom
ω
ω
⊢
N
∪
ω
∖
N
=
ω
∖
N
∪
N
40
difsnid
ω
ω
ω
⊢
N
∈
ω
→
ω
∖
N
∪
N
=
ω
41
39
40
eqtr2id
ω
ω
ω
⊢
N
∈
ω
→
ω
=
N
∪
ω
∖
N
42
41
3ad2ant1
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
→
ω
=
N
∪
ω
∖
N
43
42
ad2antrr
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
ω
=
N
∪
ω
∖
N
44
43
oveq2d
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
M
ω
=
M
N
∪
ω
∖
N
45
38
44
eleqtrrd
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
z
∪
a
↾
ω
∖
N
∈
M
ω
46
ibar
ω
ω
ω
ω
ω
ω
ω
ω
⊢
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
N
z
∪
a
↾
ω
∖
N
∈
M
ω
∧
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
47
46
adantl
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
N
z
∪
a
↾
ω
∖
N
∈
M
ω
∧
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
48
47
bicomd
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
∈
M
ω
∧
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
49
simpll1
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
∈
ω
50
eqid
ω
ω
⊢
N
z
∪
a
↾
ω
∖
N
=
N
z
∪
a
↾
ω
∖
N
51
49
9
50
fvsnun1
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
z
∪
a
↾
ω
∖
N
N
=
z
52
51
adantr
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
=
z
53
52
52
breq12d
ω
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
N
↔
z
E
z
54
53
adantl
ω
ω
ω
ω
ω
ω
ω
ω
⊢
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
N
↔
z
E
z
55
fveq2
ω
ω
⊢
J
=
N
→
N
z
∪
a
↾
ω
∖
N
J
=
N
z
∪
a
↾
ω
∖
N
N
56
55
breq2d
ω
ω
ω
ω
⊢
J
=
N
→
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
↔
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
N
57
ifptru
⊢
J
=
N
→
if-
J
=
N
z
E
z
z
E
a
J
↔
z
E
z
58
56
57
bibi12d
ω
ω
ω
ω
⊢
J
=
N
→
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
z
E
z
z
E
a
J
↔
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
N
↔
z
E
z
59
58
adantr
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
⊢
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
z
E
z
z
E
a
J
↔
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
N
↔
z
E
z
60
54
59
mpbird
ω
ω
ω
ω
ω
ω
ω
ω
⊢
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
z
E
z
z
E
a
J
61
52
adantl
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
=
z
62
49
adantr
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
∈
ω
63
62
adantl
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
∈
ω
64
9
adantr
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
z
∈
M
65
64
adantl
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
z
∈
M
66
neqne
⊢
¬
J
=
N
→
J
≠
N
67
simpll3
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
J
∈
ω
68
67
adantr
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
J
∈
ω
69
66
68
anim12ci
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
J
∈
ω
∧
J
≠
N
70
eldifsn
ω
ω
⊢
J
∈
ω
∖
N
↔
J
∈
ω
∧
J
≠
N
71
69
70
sylibr
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
J
∈
ω
∖
N
72
63
65
50
71
fvsnun2
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
J
=
a
J
73
61
72
breq12d
ω
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
↔
z
E
a
J
74
ifpfal
⊢
¬
J
=
N
→
if-
J
=
N
z
E
z
z
E
a
J
↔
z
E
a
J
75
74
bicomd
⊢
¬
J
=
N
→
z
E
a
J
↔
if-
J
=
N
z
E
z
z
E
a
J
76
75
adantr
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
z
E
a
J
↔
if-
J
=
N
z
E
z
z
E
a
J
77
73
76
bitrd
ω
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
z
E
z
z
E
a
J
78
60
77
pm2.61ian
ω
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
z
E
z
z
E
a
J
79
78
adantl
ω
ω
ω
ω
ω
ω
ω
ω
⊢
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
z
E
z
z
E
a
J
80
fveq2
ω
ω
⊢
I
=
N
→
N
z
∪
a
↾
ω
∖
N
I
=
N
z
∪
a
↾
ω
∖
N
N
81
80
breq1d
ω
ω
ω
ω
⊢
I
=
N
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
82
ifptru
⊢
I
=
N
→
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
↔
if-
J
=
N
z
E
z
z
E
a
J
83
81
82
bibi12d
ω
ω
ω
ω
⊢
I
=
N
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
↔
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
z
E
z
z
E
a
J
84
83
adantr
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
⊢
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
↔
N
z
∪
a
↾
ω
∖
N
N
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
z
E
z
z
E
a
J
85
79
84
mpbird
ω
ω
ω
ω
ω
ω
ω
ω
⊢
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
86
62
adantl
ω
ω
ω
ω
ω
ω
ω
⊢
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
∈
ω
87
64
adantl
ω
ω
ω
ω
ω
ω
⊢
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
z
∈
M
88
neqne
⊢
¬
I
=
N
→
I
≠
N
89
simpll2
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
I
∈
ω
90
89
adantr
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
I
∈
ω
91
88
90
anim12ci
ω
ω
ω
ω
ω
ω
ω
⊢
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
I
∈
ω
∧
I
≠
N
92
eldifsn
ω
ω
⊢
I
∈
ω
∖
N
↔
I
∈
ω
∧
I
≠
N
93
91
92
sylibr
ω
ω
ω
ω
ω
ω
ω
⊢
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
I
∈
ω
∖
N
94
86
87
50
93
fvsnun2
ω
ω
ω
ω
ω
ω
ω
⊢
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
=
a
I
95
52
adantl
ω
ω
ω
ω
ω
ω
ω
⊢
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
N
=
z
96
94
95
breq12d
ω
ω
ω
ω
ω
ω
ω
ω
⊢
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
N
↔
a
I
E
z
97
96
adantl
ω
ω
ω
ω
ω
ω
ω
ω
⊢
J
=
N
∧
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
N
↔
a
I
E
z
98
55
breq2d
ω
ω
ω
ω
⊢
J
=
N
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
N
99
ifptru
⊢
J
=
N
→
if-
J
=
N
a
I
E
z
a
I
E
a
J
↔
a
I
E
z
100
98
99
bibi12d
ω
ω
ω
ω
⊢
J
=
N
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
a
I
E
z
a
I
E
a
J
↔
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
N
↔
a
I
E
z
101
100
adantr
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
⊢
J
=
N
∧
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
a
I
E
z
a
I
E
a
J
↔
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
N
↔
a
I
E
z
102
97
101
mpbird
ω
ω
ω
ω
ω
ω
ω
ω
⊢
J
=
N
∧
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
a
I
E
z
a
I
E
a
J
103
94
adantl
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
=
a
I
104
72
adantrl
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
J
=
a
J
105
103
104
breq12d
ω
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
a
I
E
a
J
106
ifpfal
⊢
¬
J
=
N
→
if-
J
=
N
a
I
E
z
a
I
E
a
J
↔
a
I
E
a
J
107
106
bicomd
⊢
¬
J
=
N
→
a
I
E
a
J
↔
if-
J
=
N
a
I
E
z
a
I
E
a
J
108
107
adantr
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
a
I
E
a
J
↔
if-
J
=
N
a
I
E
z
a
I
E
a
J
109
105
108
bitrd
ω
ω
ω
ω
ω
ω
ω
ω
⊢
¬
J
=
N
∧
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
a
I
E
z
a
I
E
a
J
110
102
109
pm2.61ian
ω
ω
ω
ω
ω
ω
ω
ω
⊢
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
J
=
N
a
I
E
z
a
I
E
a
J
111
ifpfal
⊢
¬
I
=
N
→
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
↔
if-
J
=
N
a
I
E
z
a
I
E
a
J
112
111
bicomd
⊢
¬
I
=
N
→
if-
J
=
N
a
I
E
z
a
I
E
a
J
↔
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
113
112
adantr
ω
ω
ω
ω
ω
ω
⊢
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
if-
J
=
N
a
I
E
z
a
I
E
a
J
↔
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
114
110
113
bitrd
ω
ω
ω
ω
ω
ω
ω
ω
⊢
¬
I
=
N
∧
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
115
85
114
pm2.61ian
ω
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
116
48
115
bitrd
ω
ω
ω
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
∧
N
z
∪
a
↾
ω
∖
N
∈
M
ω
→
N
z
∪
a
↾
ω
∖
N
∈
M
ω
∧
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
117
45
116
mpdan
ω
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
z
∪
a
↾
ω
∖
N
∈
M
ω
∧
N
z
∪
a
↾
ω
∖
N
I
E
N
z
∪
a
↾
ω
∖
N
J
↔
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
118
5
117
bitrd
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
∧
z
∈
M
→
N
z
∪
a
↾
ω
∖
N
∈
b
∈
M
ω
|
b
I
E
b
J
↔
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
119
118
ralbidva
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
∧
a
∈
M
ω
→
∀
z
∈
M
N
z
∪
a
↾
ω
∖
N
∈
b
∈
M
ω
|
b
I
E
b
J
↔
∀
z
∈
M
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J
120
119
rabbidva
ω
ω
ω
ω
ω
ω
ω
⊢
N
∈
ω
∧
I
∈
ω
∧
J
∈
ω
→
a
∈
M
ω
|
∀
z
∈
M
N
z
∪
a
↾
ω
∖
N
∈
b
∈
M
ω
|
b
I
E
b
J
=
a
∈
M
ω
|
∀
z
∈
M
if-
I
=
N
if-
J
=
N
z
E
z
z
E
a
J
if-
J
=
N
a
I
E
z
a
I
E
a
J