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 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 ) )