Metamath Proof Explorer

Theorem bnj1417

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1417.1 
|- ( ph <-> R _FrSe A )
bnj1417.2 
|- ( ps <-> -. x e. _trCl ( x , A , R ) )
bnj1417.3 
|- ( ch <-> A. y e. A ( y R x -> [. y / x ]. ps ) )
bnj1417.4 
|- ( th <-> ( ph /\ x e. A /\ ch ) )
bnj1417.5 
|- B = ( _pred ( x , A , R ) u. U_ y e. _pred ( x , A , R ) _trCl ( y , A , R ) )
Assertion bnj1417 
|- ( ph -> A. x e. A -. x e. _trCl ( x , A , R ) )

Proof

Step Hyp Ref Expression
1 bnj1417.1 
 |-  ( ph <-> R _FrSe A )
2 bnj1417.2 
 |-  ( ps <-> -. x e. _trCl ( x , A , R ) )
3 bnj1417.3 
 |-  ( ch <-> A. y e. A ( y R x -> [. y / x ]. ps ) )
4 bnj1417.4 
 |-  ( th <-> ( ph /\ x e. A /\ ch ) )
5 bnj1417.5 
 |-  B = ( _pred ( x , A , R ) u. U_ y e. _pred ( x , A , R ) _trCl ( y , A , R ) )
6 1 biimpi 
 |-  ( ph -> R _FrSe A )
7 bnj1418 
 |-  ( x e. _pred ( x , A , R ) -> x R x )
8 7 adantl 
 |-  ( ( th /\ x e. _pred ( x , A , R ) ) -> x R x )
9 4 6 bnj835 
 |-  ( th -> R _FrSe A )
10 df-bnj15 
 |-  ( R _FrSe A <-> ( R Fr A /\ R _Se A ) )
11 10 simplbi 
 |-  ( R _FrSe A -> R Fr A )
12 9 11 syl 
 |-  ( th -> R Fr A )
13 bnj213 
 |-  _pred ( x , A , R ) C_ A
14 13 sseli 
 |-  ( x e. _pred ( x , A , R ) -> x e. A )
15 frirr 
 |-  ( ( R Fr A /\ x e. A ) -> -. x R x )
16 12 14 15 syl2an 
 |-  ( ( th /\ x e. _pred ( x , A , R ) ) -> -. x R x )
17 8 16 pm2.65da 
 |-  ( th -> -. x e. _pred ( x , A , R ) )
18 nfv 
 |-  F/ y ph
19 nfv 
 |-  F/ y x e. A
20 3 bnj1095 
 |-  ( ch -> A. y ch )
21 20 nf5i 
 |-  F/ y ch
22 18 19 21 nf3an 
 |-  F/ y ( ph /\ x e. A /\ ch )
23 4 22 nfxfr 
 |-  F/ y th
24 9 ad2antrr 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> R _FrSe A )
25 simplr 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> y e. _pred ( x , A , R ) )
26 13 25 sselid 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> y e. A )
27 simpr 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> x e. _trCl ( y , A , R ) )
28 bnj1125 
 |-  ( ( R _FrSe A /\ y e. A /\ x e. _trCl ( y , A , R ) ) -> _trCl ( x , A , R ) C_ _trCl ( y , A , R ) )
29 24 26 27 28 syl3anc 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> _trCl ( x , A , R ) C_ _trCl ( y , A , R ) )
30 bnj1147 
 |-  _trCl ( y , A , R ) C_ A
31 30 27 sselid 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> x e. A )
32 bnj906 
 |-  ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) C_ _trCl ( x , A , R ) )
33 24 31 32 syl2anc 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> _pred ( x , A , R ) C_ _trCl ( x , A , R ) )
34 33 25 sseldd 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> y e. _trCl ( x , A , R ) )
35 29 34 sseldd 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> y e. _trCl ( y , A , R ) )
36 3 biimpi 
 |-  ( ch -> A. y e. A ( y R x -> [. y / x ]. ps ) )
37 4 36 bnj837 
 |-  ( th -> A. y e. A ( y R x -> [. y / x ]. ps ) )
38 37 ad2antrr 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> A. y e. A ( y R x -> [. y / x ]. ps ) )
39 bnj1418 
 |-  ( y e. _pred ( x , A , R ) -> y R x )
40 39 ad2antlr 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> y R x )
41 rsp 
 |-  ( A. y e. A ( y R x -> [. y / x ]. ps ) -> ( y e. A -> ( y R x -> [. y / x ]. ps ) ) )
42 38 26 40 41 syl3c 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> [. y / x ]. ps )
43 vex 
 |-  y e. _V
44 eleq1w 
 |-  ( x = y -> ( x e. _trCl ( x , A , R ) <-> y e. _trCl ( x , A , R ) ) )
45 bnj1318 
 |-  ( x = y -> _trCl ( x , A , R ) = _trCl ( y , A , R ) )
46 45 eleq2d 
 |-  ( x = y -> ( y e. _trCl ( x , A , R ) <-> y e. _trCl ( y , A , R ) ) )
47 44 46 bitrd 
 |-  ( x = y -> ( x e. _trCl ( x , A , R ) <-> y e. _trCl ( y , A , R ) ) )
48 47 notbid 
 |-  ( x = y -> ( -. x e. _trCl ( x , A , R ) <-> -. y e. _trCl ( y , A , R ) ) )
49 2 48 bitrid 
 |-  ( x = y -> ( ps <-> -. y e. _trCl ( y , A , R ) ) )
50 43 49 sbcie 
 |-  ( [. y / x ]. ps <-> -. y e. _trCl ( y , A , R ) )
51 42 50 sylib 
 |-  ( ( ( th /\ y e. _pred ( x , A , R ) ) /\ x e. _trCl ( y , A , R ) ) -> -. y e. _trCl ( y , A , R ) )
52 35 51 pm2.65da 
 |-  ( ( th /\ y e. _pred ( x , A , R ) ) -> -. x e. _trCl ( y , A , R ) )
53 52 ex 
 |-  ( th -> ( y e. _pred ( x , A , R ) -> -. x e. _trCl ( y , A , R ) ) )
54 23 53 ralrimi 
 |-  ( th -> A. y e. _pred ( x , A , R ) -. x e. _trCl ( y , A , R ) )
55 ralnex 
 |-  ( A. y e. _pred ( x , A , R ) -. x e. _trCl ( y , A , R ) <-> -. E. y e. _pred ( x , A , R ) x e. _trCl ( y , A , R ) )
56 54 55 sylib 
 |-  ( th -> -. E. y e. _pred ( x , A , R ) x e. _trCl ( y , A , R ) )
57 eliun 
 |-  ( x e. U_ y e. _pred ( x , A , R ) _trCl ( y , A , R ) <-> E. y e. _pred ( x , A , R ) x e. _trCl ( y , A , R ) )
58 56 57 sylnibr 
 |-  ( th -> -. x e. U_ y e. _pred ( x , A , R ) _trCl ( y , A , R ) )
59 ioran 
 |-  ( -. ( x e. _pred ( x , A , R ) \/ x e. U_ y e. _pred ( x , A , R ) _trCl ( y , A , R ) ) <-> ( -. x e. _pred ( x , A , R ) /\ -. x e. U_ y e. _pred ( x , A , R ) _trCl ( y , A , R ) ) )
60 17 58 59 sylanbrc 
 |-  ( th -> -. ( x e. _pred ( x , A , R ) \/ x e. U_ y e. _pred ( x , A , R ) _trCl ( y , A , R ) ) )
61 4 simp2bi 
 |-  ( th -> x e. A )
62 5 bnj1414 
 |-  ( ( R _FrSe A /\ x e. A ) -> _trCl ( x , A , R ) = B )
63 9 61 62 syl2anc 
 |-  ( th -> _trCl ( x , A , R ) = B )
64 63 eleq2d 
 |-  ( th -> ( x e. _trCl ( x , A , R ) <-> x e. B ) )
65 5 bnj1138 
 |-  ( x e. B <-> ( x e. _pred ( x , A , R ) \/ x e. U_ y e. _pred ( x , A , R ) _trCl ( y , A , R ) ) )
66 64 65 bitrdi 
 |-  ( th -> ( x e. _trCl ( x , A , R ) <-> ( x e. _pred ( x , A , R ) \/ x e. U_ y e. _pred ( x , A , R ) _trCl ( y , A , R ) ) ) )
67 60 66 mtbird 
 |-  ( th -> -. x e. _trCl ( x , A , R ) )
68 67 2 sylibr 
 |-  ( th -> ps )
69 4 68 sylbir 
 |-  ( ( ph /\ x e. A /\ ch ) -> ps )
70 69 3exp 
 |-  ( ph -> ( x e. A -> ( ch -> ps ) ) )
71 70 ralrimiv 
 |-  ( ph -> A. x e. A ( ch -> ps ) )
72 3 bnj1204 
 |-  ( ( R _FrSe A /\ A. x e. A ( ch -> ps ) ) -> A. x e. A ps )
73 6 71 72 syl2anc 
 |-  ( ph -> A. x e. A ps )
74 2 ralbii 
 |-  ( A. x e. A ps <-> A. x e. A -. x e. _trCl ( x , A , R ) )
75 73 74 sylib 
 |-  ( ph -> A. x e. A -. x e. _trCl ( x , A , R ) )