Metamath Proof Explorer

Theorem wefrc

Description: A nonempty subclass of a class well-ordered by membership has a minimal element. Special case of Proposition 6.26 of TakeutiZaring p. 31. (Contributed by NM, 17-Feb-2004)

Ref Expression
Assertion wefrc 
|- ( ( _E We A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )

Proof

Step Hyp Ref Expression
1 wess 
 |-  ( B C_ A -> ( _E We A -> _E We B ) )
2 n0 
 |-  ( B =/= (/) <-> E. y y e. B )
3 ineq2 
 |-  ( x = y -> ( B i^i x ) = ( B i^i y ) )
4 3 eqeq1d 
 |-  ( x = y -> ( ( B i^i x ) = (/) <-> ( B i^i y ) = (/) ) )
5 4 rspcev 
 |-  ( ( y e. B /\ ( B i^i y ) = (/) ) -> E. x e. B ( B i^i x ) = (/) )
6 5 ex 
 |-  ( y e. B -> ( ( B i^i y ) = (/) -> E. x e. B ( B i^i x ) = (/) ) )
7 6 adantl 
 |-  ( ( _E We B /\ y e. B ) -> ( ( B i^i y ) = (/) -> E. x e. B ( B i^i x ) = (/) ) )
8 inss1 
 |-  ( B i^i y ) C_ B
9 wefr 
 |-  ( _E We B -> _E Fr B )
10 vex 
 |-  y e. _V
11 10 inex2 
 |-  ( B i^i y ) e. _V
12 11 epfrc 
 |-  ( ( _E Fr B /\ ( B i^i y ) C_ B /\ ( B i^i y ) =/= (/) ) -> E. x e. ( B i^i y ) ( ( B i^i y ) i^i x ) = (/) )
13 9 12 syl3an1 
 |-  ( ( _E We B /\ ( B i^i y ) C_ B /\ ( B i^i y ) =/= (/) ) -> E. x e. ( B i^i y ) ( ( B i^i y ) i^i x ) = (/) )
14 13 3exp 
 |-  ( _E We B -> ( ( B i^i y ) C_ B -> ( ( B i^i y ) =/= (/) -> E. x e. ( B i^i y ) ( ( B i^i y ) i^i x ) = (/) ) ) )
15 8 14 mpi 
 |-  ( _E We B -> ( ( B i^i y ) =/= (/) -> E. x e. ( B i^i y ) ( ( B i^i y ) i^i x ) = (/) ) )
16 rexin 
 |-  ( E. x e. ( B i^i y ) ( ( B i^i y ) i^i x ) = (/) <-> E. x e. B ( x e. y /\ ( ( B i^i y ) i^i x ) = (/) ) )
17 15 16 imbitrdi 
 |-  ( _E We B -> ( ( B i^i y ) =/= (/) -> E. x e. B ( x e. y /\ ( ( B i^i y ) i^i x ) = (/) ) ) )
18 17 adantr 
 |-  ( ( _E We B /\ y e. B ) -> ( ( B i^i y ) =/= (/) -> E. x e. B ( x e. y /\ ( ( B i^i y ) i^i x ) = (/) ) ) )
19 elin 
 |-  ( z e. ( B i^i x ) <-> ( z e. B /\ z e. x ) )
20 df-3an 
 |-  ( ( y e. B /\ z e. B /\ x e. B ) <-> ( ( y e. B /\ z e. B ) /\ x e. B ) )
21 3anrot 
 |-  ( ( y e. B /\ z e. B /\ x e. B ) <-> ( z e. B /\ x e. B /\ y e. B ) )
22 20 21 bitr3i 
 |-  ( ( ( y e. B /\ z e. B ) /\ x e. B ) <-> ( z e. B /\ x e. B /\ y e. B ) )
23 wetrep 
 |-  ( ( _E We B /\ ( z e. B /\ x e. B /\ y e. B ) ) -> ( ( z e. x /\ x e. y ) -> z e. y ) )
24 23 expd 
 |-  ( ( _E We B /\ ( z e. B /\ x e. B /\ y e. B ) ) -> ( z e. x -> ( x e. y -> z e. y ) ) )
25 22 24 sylan2b 
 |-  ( ( _E We B /\ ( ( y e. B /\ z e. B ) /\ x e. B ) ) -> ( z e. x -> ( x e. y -> z e. y ) ) )
26 25 exp44 
 |-  ( _E We B -> ( y e. B -> ( z e. B -> ( x e. B -> ( z e. x -> ( x e. y -> z e. y ) ) ) ) ) )
27 26 imp 
 |-  ( ( _E We B /\ y e. B ) -> ( z e. B -> ( x e. B -> ( z e. x -> ( x e. y -> z e. y ) ) ) ) )
28 27 com34 
 |-  ( ( _E We B /\ y e. B ) -> ( z e. B -> ( z e. x -> ( x e. B -> ( x e. y -> z e. y ) ) ) ) )
29 28 impd 
 |-  ( ( _E We B /\ y e. B ) -> ( ( z e. B /\ z e. x ) -> ( x e. B -> ( x e. y -> z e. y ) ) ) )
30 19 29 biimtrid 
 |-  ( ( _E We B /\ y e. B ) -> ( z e. ( B i^i x ) -> ( x e. B -> ( x e. y -> z e. y ) ) ) )
31 30 imp4a 
 |-  ( ( _E We B /\ y e. B ) -> ( z e. ( B i^i x ) -> ( ( x e. B /\ x e. y ) -> z e. y ) ) )
32 31 com23 
 |-  ( ( _E We B /\ y e. B ) -> ( ( x e. B /\ x e. y ) -> ( z e. ( B i^i x ) -> z e. y ) ) )
33 32 ralrimdv 
 |-  ( ( _E We B /\ y e. B ) -> ( ( x e. B /\ x e. y ) -> A. z e. ( B i^i x ) z e. y ) )
34 dfss3 
 |-  ( ( B i^i x ) C_ y <-> A. z e. ( B i^i x ) z e. y )
35 33 34 imbitrrdi 
 |-  ( ( _E We B /\ y e. B ) -> ( ( x e. B /\ x e. y ) -> ( B i^i x ) C_ y ) )
36 dfss 
 |-  ( ( B i^i x ) C_ y <-> ( B i^i x ) = ( ( B i^i x ) i^i y ) )
37 in32 
 |-  ( ( B i^i x ) i^i y ) = ( ( B i^i y ) i^i x )
38 37 eqeq2i 
 |-  ( ( B i^i x ) = ( ( B i^i x ) i^i y ) <-> ( B i^i x ) = ( ( B i^i y ) i^i x ) )
39 36 38 sylbb 
 |-  ( ( B i^i x ) C_ y -> ( B i^i x ) = ( ( B i^i y ) i^i x ) )
40 39 eqeq1d 
 |-  ( ( B i^i x ) C_ y -> ( ( B i^i x ) = (/) <-> ( ( B i^i y ) i^i x ) = (/) ) )
41 40 biimprd 
 |-  ( ( B i^i x ) C_ y -> ( ( ( B i^i y ) i^i x ) = (/) -> ( B i^i x ) = (/) ) )
42 35 41 syl6 
 |-  ( ( _E We B /\ y e. B ) -> ( ( x e. B /\ x e. y ) -> ( ( ( B i^i y ) i^i x ) = (/) -> ( B i^i x ) = (/) ) ) )
43 42 expd 
 |-  ( ( _E We B /\ y e. B ) -> ( x e. B -> ( x e. y -> ( ( ( B i^i y ) i^i x ) = (/) -> ( B i^i x ) = (/) ) ) ) )
44 43 imp4a 
 |-  ( ( _E We B /\ y e. B ) -> ( x e. B -> ( ( x e. y /\ ( ( B i^i y ) i^i x ) = (/) ) -> ( B i^i x ) = (/) ) ) )
45 44 reximdvai 
 |-  ( ( _E We B /\ y e. B ) -> ( E. x e. B ( x e. y /\ ( ( B i^i y ) i^i x ) = (/) ) -> E. x e. B ( B i^i x ) = (/) ) )
46 18 45 syld 
 |-  ( ( _E We B /\ y e. B ) -> ( ( B i^i y ) =/= (/) -> E. x e. B ( B i^i x ) = (/) ) )
47 7 46 pm2.61dne 
 |-  ( ( _E We B /\ y e. B ) -> E. x e. B ( B i^i x ) = (/) )
48 47 ex 
 |-  ( _E We B -> ( y e. B -> E. x e. B ( B i^i x ) = (/) ) )
49 48 exlimdv 
 |-  ( _E We B -> ( E. y y e. B -> E. x e. B ( B i^i x ) = (/) ) )
50 2 49 biimtrid 
 |-  ( _E We B -> ( B =/= (/) -> E. x e. B ( B i^i x ) = (/) ) )
51 1 50 syl6com 
 |-  ( _E We A -> ( B C_ A -> ( B =/= (/) -> E. x e. B ( B i^i x ) = (/) ) ) )
52 51 3imp 
 |-  ( ( _E We A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) )