Metamath Proof Explorer

Theorem dford3lem2

Description: Lemma for dford3 . (Contributed by Stefan O'Rear, 28-Oct-2014)

Ref Expression
Assertion dford3lem2 
|- ( ( Tr x /\ A. y e. x Tr y ) -> x e. On )

Proof

Step Hyp Ref Expression
1 suctr 
 |-  ( Tr x -> Tr suc x )
2 vex 
 |-  x e. _V
3 2 sucid 
 |-  x e. suc x
4 2 sucex 
 |-  suc x e. _V
5 treq 
 |-  ( c = suc x -> ( Tr c <-> Tr suc x ) )
6 eleq2 
 |-  ( c = suc x -> ( x e. c <-> x e. suc x ) )
7 5 6 anbi12d 
 |-  ( c = suc x -> ( ( Tr c /\ x e. c ) <-> ( Tr suc x /\ x e. suc x ) ) )
8 4 7 spcev 
 |-  ( ( Tr suc x /\ x e. suc x ) -> E. c ( Tr c /\ x e. c ) )
9 1 3 8 sylancl 
 |-  ( Tr x -> E. c ( Tr c /\ x e. c ) )
10 9 adantr 
 |-  ( ( Tr x /\ A. y e. x Tr y ) -> E. c ( Tr c /\ x e. c ) )
11 simprl 
 |-  ( ( A. b e. a ( ( Tr b /\ A. y e. b Tr y ) -> b e. On ) /\ ( Tr a /\ A. y e. a Tr y ) ) -> Tr a )
12 dford3lem1 
 |-  ( ( Tr a /\ A. y e. a Tr y ) -> A. b e. a ( Tr b /\ A. y e. b Tr y ) )
13 ralim 
 |-  ( A. b e. a ( ( Tr b /\ A. y e. b Tr y ) -> b e. On ) -> ( A. b e. a ( Tr b /\ A. y e. b Tr y ) -> A. b e. a b e. On ) )
14 12 13 syl5 
 |-  ( A. b e. a ( ( Tr b /\ A. y e. b Tr y ) -> b e. On ) -> ( ( Tr a /\ A. y e. a Tr y ) -> A. b e. a b e. On ) )
15 14 imp 
 |-  ( ( A. b e. a ( ( Tr b /\ A. y e. b Tr y ) -> b e. On ) /\ ( Tr a /\ A. y e. a Tr y ) ) -> A. b e. a b e. On )
16 dfss3 
 |-  ( a C_ On <-> A. b e. a b e. On )
17 15 16 sylibr 
 |-  ( ( A. b e. a ( ( Tr b /\ A. y e. b Tr y ) -> b e. On ) /\ ( Tr a /\ A. y e. a Tr y ) ) -> a C_ On )
18 ordon 
 |-  Ord On
19 18 a1i 
 |-  ( ( A. b e. a ( ( Tr b /\ A. y e. b Tr y ) -> b e. On ) /\ ( Tr a /\ A. y e. a Tr y ) ) -> Ord On )
20 trssord 
 |-  ( ( Tr a /\ a C_ On /\ Ord On ) -> Ord a )
21 11 17 19 20 syl3anc 
 |-  ( ( A. b e. a ( ( Tr b /\ A. y e. b Tr y ) -> b e. On ) /\ ( Tr a /\ A. y e. a Tr y ) ) -> Ord a )
22 vex 
 |-  a e. _V
23 22 elon 
 |-  ( a e. On <-> Ord a )
24 21 23 sylibr 
 |-  ( ( A. b e. a ( ( Tr b /\ A. y e. b Tr y ) -> b e. On ) /\ ( Tr a /\ A. y e. a Tr y ) ) -> a e. On )
25 24 ex 
 |-  ( A. b e. a ( ( Tr b /\ A. y e. b Tr y ) -> b e. On ) -> ( ( Tr a /\ A. y e. a Tr y ) -> a e. On ) )
26 treq 
 |-  ( a = b -> ( Tr a <-> Tr b ) )
27 raleq 
 |-  ( a = b -> ( A. y e. a Tr y <-> A. y e. b Tr y ) )
28 26 27 anbi12d 
 |-  ( a = b -> ( ( Tr a /\ A. y e. a Tr y ) <-> ( Tr b /\ A. y e. b Tr y ) ) )
29 eleq1w 
 |-  ( a = b -> ( a e. On <-> b e. On ) )
30 28 29 imbi12d 
 |-  ( a = b -> ( ( ( Tr a /\ A. y e. a Tr y ) -> a e. On ) <-> ( ( Tr b /\ A. y e. b Tr y ) -> b e. On ) ) )
31 treq 
 |-  ( a = x -> ( Tr a <-> Tr x ) )
32 raleq 
 |-  ( a = x -> ( A. y e. a Tr y <-> A. y e. x Tr y ) )
33 31 32 anbi12d 
 |-  ( a = x -> ( ( Tr a /\ A. y e. a Tr y ) <-> ( Tr x /\ A. y e. x Tr y ) ) )
34 eleq1w 
 |-  ( a = x -> ( a e. On <-> x e. On ) )
35 33 34 imbi12d 
 |-  ( a = x -> ( ( ( Tr a /\ A. y e. a Tr y ) -> a e. On ) <-> ( ( Tr x /\ A. y e. x Tr y ) -> x e. On ) ) )
36 25 30 35 setindtrs 
 |-  ( E. c ( Tr c /\ x e. c ) -> ( ( Tr x /\ A. y e. x Tr y ) -> x e. On ) )
37 10 36 mpcom 
 |-  ( ( Tr x /\ A. y e. x Tr y ) -> x e. On )