Metamath Proof Explorer

Theorem wfrlem10OLD

Description: Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. When z is an R minimal element of ( A \ dom F ) , then its predecessor class is equal to dom F . (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011)

Ref Expression
Hypotheses wfrlem10OLD.1 
|- R We A
wfrlem10OLD.2 
|- F = wrecs ( R , A , G )
Assertion wfrlem10OLD 
|- ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> Pred ( R , A , z ) = dom F )

Proof

Step Hyp Ref Expression
1 wfrlem10OLD.1 
 |-  R We A
2 wfrlem10OLD.2 
 |-  F = wrecs ( R , A , G )
3 2 wfrlem8OLD 
 |-  ( Pred ( R , ( A \ dom F ) , z ) = (/) <-> Pred ( R , A , z ) = Pred ( R , dom F , z ) )
4 3 biimpi 
 |-  ( Pred ( R , ( A \ dom F ) , z ) = (/) -> Pred ( R , A , z ) = Pred ( R , dom F , z ) )
5 predss 
 |-  Pred ( R , dom F , z ) C_ dom F
6 5 a1i 
 |-  ( z e. ( A \ dom F ) -> Pred ( R , dom F , z ) C_ dom F )
7 simpr 
 |-  ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> w e. dom F )
8 eldifn 
 |-  ( z e. ( A \ dom F ) -> -. z e. dom F )
9 eleq1w 
 |-  ( w = z -> ( w e. dom F <-> z e. dom F ) )
10 9 notbid 
 |-  ( w = z -> ( -. w e. dom F <-> -. z e. dom F ) )
11 8 10 syl5ibrcom 
 |-  ( z e. ( A \ dom F ) -> ( w = z -> -. w e. dom F ) )
12 11 con2d 
 |-  ( z e. ( A \ dom F ) -> ( w e. dom F -> -. w = z ) )
13 12 imp 
 |-  ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> -. w = z )
14 ssel 
 |-  ( Pred ( R , A , w ) C_ dom F -> ( z e. Pred ( R , A , w ) -> z e. dom F ) )
15 14 con3d 
 |-  ( Pred ( R , A , w ) C_ dom F -> ( -. z e. dom F -> -. z e. Pred ( R , A , w ) ) )
16 8 15 syl5com 
 |-  ( z e. ( A \ dom F ) -> ( Pred ( R , A , w ) C_ dom F -> -. z e. Pred ( R , A , w ) ) )
17 2 wfrdmclOLD 
 |-  ( w e. dom F -> Pred ( R , A , w ) C_ dom F )
18 16 17 impel 
 |-  ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> -. z e. Pred ( R , A , w ) )
19 eldifi 
 |-  ( z e. ( A \ dom F ) -> z e. A )
20 elpredg 
 |-  ( ( w e. dom F /\ z e. A ) -> ( z e. Pred ( R , A , w ) <-> z R w ) )
21 20 ancoms 
 |-  ( ( z e. A /\ w e. dom F ) -> ( z e. Pred ( R , A , w ) <-> z R w ) )
22 19 21 sylan 
 |-  ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> ( z e. Pred ( R , A , w ) <-> z R w ) )
23 18 22 mtbid 
 |-  ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> -. z R w )
24 2 wfrdmssOLD 
 |-  dom F C_ A
25 24 sseli 
 |-  ( w e. dom F -> w e. A )
26 weso 
 |-  ( R We A -> R Or A )
27 1 26 ax-mp 
 |-  R Or A
28 solin 
 |-  ( ( R Or A /\ ( w e. A /\ z e. A ) ) -> ( w R z \/ w = z \/ z R w ) )
29 27 28 mpan 
 |-  ( ( w e. A /\ z e. A ) -> ( w R z \/ w = z \/ z R w ) )
30 25 19 29 syl2anr 
 |-  ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> ( w R z \/ w = z \/ z R w ) )
31 13 23 30 ecase23d 
 |-  ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> w R z )
32 vex 
 |-  w e. _V
33 32 elpred 
 |-  ( z e. _V -> ( w e. Pred ( R , dom F , z ) <-> ( w e. dom F /\ w R z ) ) )
34 33 elv 
 |-  ( w e. Pred ( R , dom F , z ) <-> ( w e. dom F /\ w R z ) )
35 7 31 34 sylanbrc 
 |-  ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> w e. Pred ( R , dom F , z ) )
36 6 35 eqelssd 
 |-  ( z e. ( A \ dom F ) -> Pred ( R , dom F , z ) = dom F )
37 4 36 sylan9eqr 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> Pred ( R , A , z ) = dom F )