Metamath Proof Explorer

Theorem dfon2lem6

Description: Lemma for dfon2 . A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Assertion dfon2lem6 
|- ( ( 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 ) )

Proof

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 imbitrdi 
 |-  ( 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 biimtrid 
 |-  ( ( ( ( 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 biimtrrid 
 |-  ( ( ( 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 imbitrrid 
 |-  ( 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 ) )