Step |
Hyp |
Ref |
Expression |
1 |
|
pssss |
|- ( y C. S -> y C_ S ) |
2 |
|
ssralv |
|- ( y C_ S -> ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) -> A. x e. y A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) ) |
3 |
1 2
|
syl |
|- ( y C. S -> ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) -> A. x e. y A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) ) |
4 |
3
|
impcom |
|- ( ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) /\ y C. S ) -> A. x e. y A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) |
5 |
4
|
adantrr |
|- ( ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) /\ ( y C. S /\ Tr y ) ) -> A. x e. y A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) |
6 |
5
|
ad2ant2lr |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) -> A. x e. y A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) |
7 |
|
psseq2 |
|- ( x = w -> ( z C. x <-> z C. w ) ) |
8 |
7
|
anbi1d |
|- ( x = w -> ( ( z C. x /\ Tr z ) <-> ( z C. w /\ Tr z ) ) ) |
9 |
|
elequ2 |
|- ( x = w -> ( z e. x <-> z e. w ) ) |
10 |
8 9
|
imbi12d |
|- ( x = w -> ( ( ( z C. x /\ Tr z ) -> z e. x ) <-> ( ( z C. w /\ Tr z ) -> z e. w ) ) ) |
11 |
10
|
albidv |
|- ( x = w -> ( A. z ( ( z C. x /\ Tr z ) -> z e. x ) <-> A. z ( ( z C. w /\ Tr z ) -> z e. w ) ) ) |
12 |
11
|
rspccv |
|- ( A. x e. y A. z ( ( z C. x /\ Tr z ) -> z e. x ) -> ( w e. y -> A. z ( ( z C. w /\ Tr z ) -> z e. w ) ) ) |
13 |
6 12
|
syl |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) -> ( w e. y -> A. z ( ( z C. w /\ Tr z ) -> z e. w ) ) ) |
14 |
13
|
imp |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) /\ w e. y ) -> A. z ( ( z C. w /\ Tr z ) -> z e. w ) ) |
15 |
|
eldifi |
|- ( s e. ( S \ y ) -> s e. S ) |
16 |
|
psseq2 |
|- ( x = s -> ( z C. x <-> z C. s ) ) |
17 |
16
|
anbi1d |
|- ( x = s -> ( ( z C. x /\ Tr z ) <-> ( z C. s /\ Tr z ) ) ) |
18 |
|
elequ2 |
|- ( x = s -> ( z e. x <-> z e. s ) ) |
19 |
17 18
|
imbi12d |
|- ( x = s -> ( ( ( z C. x /\ Tr z ) -> z e. x ) <-> ( ( z C. s /\ Tr z ) -> z e. s ) ) ) |
20 |
19
|
albidv |
|- ( x = s -> ( A. z ( ( z C. x /\ Tr z ) -> z e. x ) <-> A. z ( ( z C. s /\ Tr z ) -> z e. s ) ) ) |
21 |
20
|
rspcv |
|- ( s e. S -> ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) -> A. z ( ( z C. s /\ Tr z ) -> z e. s ) ) ) |
22 |
15 21
|
syl |
|- ( s e. ( S \ y ) -> ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) -> A. z ( ( z C. s /\ Tr z ) -> z e. s ) ) ) |
23 |
|
psseq1 |
|- ( z = t -> ( z C. s <-> t C. s ) ) |
24 |
|
treq |
|- ( z = t -> ( Tr z <-> Tr t ) ) |
25 |
23 24
|
anbi12d |
|- ( z = t -> ( ( z C. s /\ Tr z ) <-> ( t C. s /\ Tr t ) ) ) |
26 |
|
elequ1 |
|- ( z = t -> ( z e. s <-> t e. s ) ) |
27 |
25 26
|
imbi12d |
|- ( z = t -> ( ( ( z C. s /\ Tr z ) -> z e. s ) <-> ( ( t C. s /\ Tr t ) -> t e. s ) ) ) |
28 |
27
|
cbvalvw |
|- ( A. z ( ( z C. s /\ Tr z ) -> z e. s ) <-> A. t ( ( t C. s /\ Tr t ) -> t e. s ) ) |
29 |
22 28
|
syl6ib |
|- ( s e. ( S \ y ) -> ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) -> A. t ( ( t C. s /\ Tr t ) -> t e. s ) ) ) |
30 |
29
|
impcom |
|- ( ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) /\ s e. ( S \ y ) ) -> A. t ( ( t C. s /\ Tr t ) -> t e. s ) ) |
31 |
30
|
ad2ant2l |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) -> A. t ( ( t C. s /\ Tr t ) -> t e. s ) ) |
32 |
31
|
adantr |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) /\ w e. y ) -> A. t ( ( t C. s /\ Tr t ) -> t e. s ) ) |
33 |
|
vex |
|- w e. _V |
34 |
|
vex |
|- s e. _V |
35 |
33 34
|
dfon2lem5 |
|- ( ( A. z ( ( z C. w /\ Tr z ) -> z e. w ) /\ A. t ( ( t C. s /\ Tr t ) -> t e. s ) ) -> ( w e. s \/ w = s \/ s e. w ) ) |
36 |
|
3orrot |
|- ( ( w e. s \/ w = s \/ s e. w ) <-> ( w = s \/ s e. w \/ w e. s ) ) |
37 |
|
3orass |
|- ( ( w = s \/ s e. w \/ w e. s ) <-> ( w = s \/ ( s e. w \/ w e. s ) ) ) |
38 |
36 37
|
bitri |
|- ( ( w e. s \/ w = s \/ s e. w ) <-> ( w = s \/ ( s e. w \/ w e. s ) ) ) |
39 |
|
eleq1a |
|- ( s e. ( S \ y ) -> ( w = s -> w e. ( S \ y ) ) ) |
40 |
|
elndif |
|- ( w e. y -> -. w e. ( S \ y ) ) |
41 |
39 40
|
nsyli |
|- ( s e. ( S \ y ) -> ( w e. y -> -. w = s ) ) |
42 |
41
|
imp |
|- ( ( s e. ( S \ y ) /\ w e. y ) -> -. w = s ) |
43 |
42
|
adantll |
|- ( ( ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) /\ w e. y ) -> -. w = s ) |
44 |
43
|
adantll |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) /\ w e. y ) -> -. w = s ) |
45 |
|
orel1 |
|- ( -. w = s -> ( ( w = s \/ ( s e. w \/ w e. s ) ) -> ( s e. w \/ w e. s ) ) ) |
46 |
|
trss |
|- ( Tr y -> ( w e. y -> w C_ y ) ) |
47 |
|
eldifn |
|- ( s e. ( S \ y ) -> -. s e. y ) |
48 |
|
ssel |
|- ( w C_ y -> ( s e. w -> s e. y ) ) |
49 |
48
|
con3d |
|- ( w C_ y -> ( -. s e. y -> -. s e. w ) ) |
50 |
47 49
|
syl5com |
|- ( s e. ( S \ y ) -> ( w C_ y -> -. s e. w ) ) |
51 |
46 50
|
syl9 |
|- ( Tr y -> ( s e. ( S \ y ) -> ( w e. y -> -. s e. w ) ) ) |
52 |
51
|
adantl |
|- ( ( y C. S /\ Tr y ) -> ( s e. ( S \ y ) -> ( w e. y -> -. s e. w ) ) ) |
53 |
52
|
imp31 |
|- ( ( ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) /\ w e. y ) -> -. s e. w ) |
54 |
53
|
adantll |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) /\ w e. y ) -> -. s e. w ) |
55 |
|
orel1 |
|- ( -. s e. w -> ( ( s e. w \/ w e. s ) -> w e. s ) ) |
56 |
54 55
|
syl |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) /\ w e. y ) -> ( ( s e. w \/ w e. s ) -> w e. s ) ) |
57 |
45 56
|
syl9r |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) /\ w e. y ) -> ( -. w = s -> ( ( w = s \/ ( s e. w \/ w e. s ) ) -> w e. s ) ) ) |
58 |
44 57
|
mpd |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) /\ w e. y ) -> ( ( w = s \/ ( s e. w \/ w e. s ) ) -> w e. s ) ) |
59 |
38 58
|
syl5bi |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) /\ w e. y ) -> ( ( w e. s \/ w = s \/ s e. w ) -> w e. s ) ) |
60 |
35 59
|
syl5 |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) /\ w e. y ) -> ( ( A. z ( ( z C. w /\ Tr z ) -> z e. w ) /\ A. t ( ( t C. s /\ Tr t ) -> t e. s ) ) -> w e. s ) ) |
61 |
14 32 60
|
mp2and |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) /\ w e. y ) -> w e. s ) |
62 |
61
|
ex |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) -> ( w e. y -> w e. s ) ) |
63 |
62
|
ssrdv |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) -> y C_ s ) |
64 |
|
dfpss2 |
|- ( y C. s <-> ( y C_ s /\ -. y = s ) ) |
65 |
|
psseq1 |
|- ( z = y -> ( z C. s <-> y C. s ) ) |
66 |
|
treq |
|- ( z = y -> ( Tr z <-> Tr y ) ) |
67 |
65 66
|
anbi12d |
|- ( z = y -> ( ( z C. s /\ Tr z ) <-> ( y C. s /\ Tr y ) ) ) |
68 |
|
elequ1 |
|- ( z = y -> ( z e. s <-> y e. s ) ) |
69 |
67 68
|
imbi12d |
|- ( z = y -> ( ( ( z C. s /\ Tr z ) -> z e. s ) <-> ( ( y C. s /\ Tr y ) -> y e. s ) ) ) |
70 |
69
|
spvv |
|- ( A. z ( ( z C. s /\ Tr z ) -> z e. s ) -> ( ( y C. s /\ Tr y ) -> y e. s ) ) |
71 |
70
|
expd |
|- ( A. z ( ( z C. s /\ Tr z ) -> z e. s ) -> ( y C. s -> ( Tr y -> y e. s ) ) ) |
72 |
71
|
com23 |
|- ( A. z ( ( z C. s /\ Tr z ) -> z e. s ) -> ( Tr y -> ( y C. s -> y e. s ) ) ) |
73 |
22 72
|
syl6 |
|- ( s e. ( S \ y ) -> ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) -> ( Tr y -> ( y C. s -> y e. s ) ) ) ) |
74 |
73
|
com3l |
|- ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) -> ( Tr y -> ( s e. ( S \ y ) -> ( y C. s -> y e. s ) ) ) ) |
75 |
74
|
adantld |
|- ( A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) -> ( ( y C. S /\ Tr y ) -> ( s e. ( S \ y ) -> ( y C. s -> y e. s ) ) ) ) |
76 |
75
|
adantl |
|- ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) -> ( ( y C. S /\ Tr y ) -> ( s e. ( S \ y ) -> ( y C. s -> y e. s ) ) ) ) |
77 |
76
|
imp32 |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) -> ( y C. s -> y e. s ) ) |
78 |
64 77
|
syl5bir |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) -> ( ( y C_ s /\ -. y = s ) -> y e. s ) ) |
79 |
63 78
|
mpand |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) -> ( -. y = s -> y e. s ) ) |
80 |
79
|
orrd |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( ( y C. S /\ Tr y ) /\ s e. ( S \ y ) ) ) -> ( y = s \/ y e. s ) ) |
81 |
80
|
anassrs |
|- ( ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( y C. S /\ Tr y ) ) /\ s e. ( S \ y ) ) -> ( y = s \/ y e. s ) ) |
82 |
81
|
ralrimiva |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( y C. S /\ Tr y ) ) -> A. s e. ( S \ y ) ( y = s \/ y e. s ) ) |
83 |
|
pssdif |
|- ( y C. S -> ( S \ y ) =/= (/) ) |
84 |
|
r19.2z |
|- ( ( ( S \ y ) =/= (/) /\ A. s e. ( S \ y ) ( y = s \/ y e. s ) ) -> E. s e. ( S \ y ) ( y = s \/ y e. s ) ) |
85 |
84
|
ex |
|- ( ( S \ y ) =/= (/) -> ( A. s e. ( S \ y ) ( y = s \/ y e. s ) -> E. s e. ( S \ y ) ( y = s \/ y e. s ) ) ) |
86 |
83 85
|
syl |
|- ( y C. S -> ( A. s e. ( S \ y ) ( y = s \/ y e. s ) -> E. s e. ( S \ y ) ( y = s \/ y e. s ) ) ) |
87 |
86
|
ad2antrl |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( y C. S /\ Tr y ) ) -> ( A. s e. ( S \ y ) ( y = s \/ y e. s ) -> E. s e. ( S \ y ) ( y = s \/ y e. s ) ) ) |
88 |
|
eleq1w |
|- ( y = s -> ( y e. S <-> s e. S ) ) |
89 |
15 88
|
syl5ibr |
|- ( y = s -> ( s e. ( S \ y ) -> y e. S ) ) |
90 |
89
|
a1i |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( y C. S /\ Tr y ) ) -> ( y = s -> ( s e. ( S \ y ) -> y e. S ) ) ) |
91 |
|
trel |
|- ( Tr S -> ( ( y e. s /\ s e. S ) -> y e. S ) ) |
92 |
91
|
expd |
|- ( Tr S -> ( y e. s -> ( s e. S -> y e. S ) ) ) |
93 |
15 92
|
syl7 |
|- ( Tr S -> ( y e. s -> ( s e. ( S \ y ) -> y e. S ) ) ) |
94 |
93
|
ad2antrr |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( y C. S /\ Tr y ) ) -> ( y e. s -> ( s e. ( S \ y ) -> y e. S ) ) ) |
95 |
90 94
|
jaod |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( y C. S /\ Tr y ) ) -> ( ( y = s \/ y e. s ) -> ( s e. ( S \ y ) -> y e. S ) ) ) |
96 |
95
|
com23 |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( y C. S /\ Tr y ) ) -> ( s e. ( S \ y ) -> ( ( y = s \/ y e. s ) -> y e. S ) ) ) |
97 |
96
|
rexlimdv |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( y C. S /\ Tr y ) ) -> ( E. s e. ( S \ y ) ( y = s \/ y e. s ) -> y e. S ) ) |
98 |
87 97
|
syld |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( y C. S /\ Tr y ) ) -> ( A. s e. ( S \ y ) ( y = s \/ y e. s ) -> y e. S ) ) |
99 |
82 98
|
mpd |
|- ( ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) /\ ( y C. S /\ Tr y ) ) -> y e. S ) |
100 |
99
|
ex |
|- ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) -> ( ( y C. S /\ Tr y ) -> y e. S ) ) |
101 |
100
|
alrimiv |
|- ( ( Tr S /\ A. x e. S A. z ( ( z C. x /\ Tr z ) -> z e. x ) ) -> A. y ( ( y C. S /\ Tr y ) -> y e. S ) ) |