Step |
Hyp |
Ref |
Expression |
1 |
|
gneispace.a |
|
2 |
1
|
gneispace3 |
|
3 |
|
simpll |
|
4 |
|
simplr |
|
5 |
|
difss |
|
6 |
|
difss |
|
7 |
6
|
sspwi |
|
8 |
5 7
|
sstri |
|
9 |
4 8
|
sstrdi |
|
10 |
|
simpr |
|
11 |
|
simpl |
|
12 |
|
fvelrn |
|
13 |
11 12
|
sylan |
|
14 |
|
ssel2 |
|
15 |
|
eldifsni |
|
16 |
14 15
|
syl |
|
17 |
10 13 16
|
syl2an2r |
|
18 |
17
|
ralrimiva |
|
19 |
|
r19.26 |
|
20 |
19
|
biimpri |
|
21 |
18 20
|
sylan |
|
22 |
3 9 21
|
3jca |
|
23 |
|
simp1 |
|
24 |
|
nfv |
|
25 |
|
nfv |
|
26 |
|
nfra1 |
|
27 |
24 25 26
|
nf3an |
|
28 |
|
simpr |
|
29 |
|
simpl |
|
30 |
29
|
19.8ad |
|
31 |
30
|
ralimi |
|
32 |
28 31
|
syl |
|
33 |
32
|
ralimi |
|
34 |
33
|
3ad2ant3 |
|
35 |
|
rsp |
|
36 |
34 35
|
syl |
|
37 |
|
df-ex |
|
38 |
37
|
ralbii |
|
39 |
|
ralnex |
|
40 |
38 39
|
bitri |
|
41 |
|
0el |
|
42 |
40 41
|
xchbinxr |
|
43 |
42
|
biimpi |
|
44 |
|
elinel1 |
|
45 |
43 44
|
nsyl |
|
46 |
|
disjsn |
|
47 |
45 46
|
sylibr |
|
48 |
|
disjdif2 |
|
49 |
47 48
|
syl |
|
50 |
36 49
|
syl6 |
|
51 |
|
simp2 |
|
52 |
12
|
ex |
|
53 |
23 52
|
syl |
|
54 |
|
ssel2 |
|
55 |
|
fvex |
|
56 |
55
|
elpw |
|
57 |
|
df-ss |
|
58 |
56 57
|
sylbb |
|
59 |
54 58
|
syl |
|
60 |
51 53 59
|
syl6an |
|
61 |
50 60
|
jcad |
|
62 |
|
eqtr |
|
63 |
|
df-ss |
|
64 |
|
indif2 |
|
65 |
64
|
eqeq1i |
|
66 |
63 65
|
bitri |
|
67 |
62 66
|
sylibr |
|
68 |
61 67
|
syl6 |
|
69 |
27 68
|
ralrimi |
|
70 |
23
|
funfnd |
|
71 |
|
sseq1 |
|
72 |
71
|
ralrn |
|
73 |
70 72
|
syl |
|
74 |
69 73
|
mpbird |
|
75 |
|
pwssb |
|
76 |
74 75
|
sylibr |
|
77 |
|
simpl |
|
78 |
77
|
ralimi |
|
79 |
78
|
3ad2ant3 |
|
80 |
23 79
|
jca |
|
81 |
|
elrnrexdm |
|
82 |
|
nesym |
|
83 |
82
|
ralbii |
|
84 |
|
ralnex |
|
85 |
83 84
|
sylbb |
|
86 |
81 85
|
nsyli |
|
87 |
86
|
imp |
|
88 |
|
disjsn |
|
89 |
87 88
|
sylibr |
|
90 |
80 89
|
syl |
|
91 |
|
reldisj |
|
92 |
91
|
biimpd |
|
93 |
76 90 92
|
sylc |
|
94 |
23 93
|
jca |
|
95 |
19
|
biimpi |
|
96 |
95
|
3ad2ant3 |
|
97 |
|
simpr |
|
98 |
96 97
|
syl |
|
99 |
94 98
|
jca |
|
100 |
22 99
|
impbii |
|
101 |
2 100
|
syl6bb |
|