Metamath Proof Explorer

Theorem epfrs

Description: The strong form of the Axiom of Regularity (no sethood requirement on A ), with the axiom itself present as an antecedent. See also zfregs . (Contributed by Mario Carneiro, 22-Mar-2013)

Ref Expression
Assertion epfrs 
|- ( ( _E Fr A /\ A =/= (/) ) -> E. x e. A ( x i^i A ) = (/) )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( A =/= (/) <-> E. z z e. A )
2 snssi 
 |-  ( z e. A -> { z } C_ A )
3 2 anim2i 
 |-  ( ( { z } C_ y /\ z e. A ) -> ( { z } C_ y /\ { z } C_ A ) )
4 ssin 
 |-  ( ( { z } C_ y /\ { z } C_ A ) <-> { z } C_ ( y i^i A ) )
5 vex 
 |-  z e. _V
6 5 snss 
 |-  ( z e. ( y i^i A ) <-> { z } C_ ( y i^i A ) )
7 4 6 bitr4i 
 |-  ( ( { z } C_ y /\ { z } C_ A ) <-> z e. ( y i^i A ) )
8 3 7 sylib 
 |-  ( ( { z } C_ y /\ z e. A ) -> z e. ( y i^i A ) )
9 8 ne0d 
 |-  ( ( { z } C_ y /\ z e. A ) -> ( y i^i A ) =/= (/) )
10 inss2 
 |-  ( y i^i A ) C_ A
11 vex 
 |-  y e. _V
12 11 inex1 
 |-  ( y i^i A ) e. _V
13 12 epfrc 
 |-  ( ( _E Fr A /\ ( y i^i A ) C_ A /\ ( y i^i A ) =/= (/) ) -> E. x e. ( y i^i A ) ( ( y i^i A ) i^i x ) = (/) )
14 10 13 mp3an2 
 |-  ( ( _E Fr A /\ ( y i^i A ) =/= (/) ) -> E. x e. ( y i^i A ) ( ( y i^i A ) i^i x ) = (/) )
15 elin 
 |-  ( x e. ( y i^i A ) <-> ( x e. y /\ x e. A ) )
16 15 anbi1i 
 |-  ( ( x e. ( y i^i A ) /\ ( ( y i^i A ) i^i x ) = (/) ) <-> ( ( x e. y /\ x e. A ) /\ ( ( y i^i A ) i^i x ) = (/) ) )
17 anass 
 |-  ( ( ( x e. y /\ x e. A ) /\ ( ( y i^i A ) i^i x ) = (/) ) <-> ( x e. y /\ ( x e. A /\ ( ( y i^i A ) i^i x ) = (/) ) ) )
18 16 17 bitri 
 |-  ( ( x e. ( y i^i A ) /\ ( ( y i^i A ) i^i x ) = (/) ) <-> ( x e. y /\ ( x e. A /\ ( ( y i^i A ) i^i x ) = (/) ) ) )
19 n0 
 |-  ( ( x i^i A ) =/= (/) <-> E. w w e. ( x i^i A ) )
20 elinel1 
 |-  ( w e. ( x i^i A ) -> w e. x )
21 20 ancri 
 |-  ( w e. ( x i^i A ) -> ( w e. x /\ w e. ( x i^i A ) ) )
22 trel 
 |-  ( Tr y -> ( ( w e. x /\ x e. y ) -> w e. y ) )
23 inass 
 |-  ( ( y i^i A ) i^i x ) = ( y i^i ( A i^i x ) )
24 incom 
 |-  ( A i^i x ) = ( x i^i A )
25 24 ineq2i 
 |-  ( y i^i ( A i^i x ) ) = ( y i^i ( x i^i A ) )
26 23 25 eqtri 
 |-  ( ( y i^i A ) i^i x ) = ( y i^i ( x i^i A ) )
27 26 eleq2i 
 |-  ( w e. ( ( y i^i A ) i^i x ) <-> w e. ( y i^i ( x i^i A ) ) )
28 elin 
 |-  ( w e. ( y i^i ( x i^i A ) ) <-> ( w e. y /\ w e. ( x i^i A ) ) )
29 27 28 bitr2i 
 |-  ( ( w e. y /\ w e. ( x i^i A ) ) <-> w e. ( ( y i^i A ) i^i x ) )
30 ne0i 
 |-  ( w e. ( ( y i^i A ) i^i x ) -> ( ( y i^i A ) i^i x ) =/= (/) )
31 29 30 sylbi 
 |-  ( ( w e. y /\ w e. ( x i^i A ) ) -> ( ( y i^i A ) i^i x ) =/= (/) )
32 31 ex 
 |-  ( w e. y -> ( w e. ( x i^i A ) -> ( ( y i^i A ) i^i x ) =/= (/) ) )
33 22 32 syl6 
 |-  ( Tr y -> ( ( w e. x /\ x e. y ) -> ( w e. ( x i^i A ) -> ( ( y i^i A ) i^i x ) =/= (/) ) ) )
34 33 expd 
 |-  ( Tr y -> ( w e. x -> ( x e. y -> ( w e. ( x i^i A ) -> ( ( y i^i A ) i^i x ) =/= (/) ) ) ) )
35 34 com34 
 |-  ( Tr y -> ( w e. x -> ( w e. ( x i^i A ) -> ( x e. y -> ( ( y i^i A ) i^i x ) =/= (/) ) ) ) )
36 35 impd 
 |-  ( Tr y -> ( ( w e. x /\ w e. ( x i^i A ) ) -> ( x e. y -> ( ( y i^i A ) i^i x ) =/= (/) ) ) )
37 21 36 syl5 
 |-  ( Tr y -> ( w e. ( x i^i A ) -> ( x e. y -> ( ( y i^i A ) i^i x ) =/= (/) ) ) )
38 37 exlimdv 
 |-  ( Tr y -> ( E. w w e. ( x i^i A ) -> ( x e. y -> ( ( y i^i A ) i^i x ) =/= (/) ) ) )
39 19 38 biimtrid 
 |-  ( Tr y -> ( ( x i^i A ) =/= (/) -> ( x e. y -> ( ( y i^i A ) i^i x ) =/= (/) ) ) )
40 39 com23 
 |-  ( Tr y -> ( x e. y -> ( ( x i^i A ) =/= (/) -> ( ( y i^i A ) i^i x ) =/= (/) ) ) )
41 40 imp 
 |-  ( ( Tr y /\ x e. y ) -> ( ( x i^i A ) =/= (/) -> ( ( y i^i A ) i^i x ) =/= (/) ) )
42 41 necon4d 
 |-  ( ( Tr y /\ x e. y ) -> ( ( ( y i^i A ) i^i x ) = (/) -> ( x i^i A ) = (/) ) )
43 42 anim2d 
 |-  ( ( Tr y /\ x e. y ) -> ( ( x e. A /\ ( ( y i^i A ) i^i x ) = (/) ) -> ( x e. A /\ ( x i^i A ) = (/) ) ) )
44 43 expimpd 
 |-  ( Tr y -> ( ( x e. y /\ ( x e. A /\ ( ( y i^i A ) i^i x ) = (/) ) ) -> ( x e. A /\ ( x i^i A ) = (/) ) ) )
45 18 44 biimtrid 
 |-  ( Tr y -> ( ( x e. ( y i^i A ) /\ ( ( y i^i A ) i^i x ) = (/) ) -> ( x e. A /\ ( x i^i A ) = (/) ) ) )
46 45 reximdv2 
 |-  ( Tr y -> ( E. x e. ( y i^i A ) ( ( y i^i A ) i^i x ) = (/) -> E. x e. A ( x i^i A ) = (/) ) )
47 14 46 syl5 
 |-  ( Tr y -> ( ( _E Fr A /\ ( y i^i A ) =/= (/) ) -> E. x e. A ( x i^i A ) = (/) ) )
48 47 expcomd 
 |-  ( Tr y -> ( ( y i^i A ) =/= (/) -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) )
49 9 48 syl5 
 |-  ( Tr y -> ( ( { z } C_ y /\ z e. A ) -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) )
50 49 expd 
 |-  ( Tr y -> ( { z } C_ y -> ( z e. A -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) ) )
51 50 impcom 
 |-  ( ( { z } C_ y /\ Tr y ) -> ( z e. A -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) )
52 51 3adant3 
 |-  ( ( { z } C_ y /\ Tr y /\ A. w ( ( { z } C_ w /\ Tr w ) -> y C_ w ) ) -> ( z e. A -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) ) )
53 vsnex 
 |-  { z } e. _V
54 53 tz9.1 
 |-  E. y ( { z } C_ y /\ Tr y /\ A. w ( ( { z } C_ w /\ Tr w ) -> y C_ w ) )
55 52 54 exlimiiv 
 |-  ( z e. A -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) )
56 55 exlimiv 
 |-  ( E. z z e. A -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) )
57 1 56 sylbi 
 |-  ( A =/= (/) -> ( _E Fr A -> E. x e. A ( x i^i A ) = (/) ) )
58 57 impcom 
 |-  ( ( _E Fr A /\ A =/= (/) ) -> E. x e. A ( x i^i A ) = (/) )