Metamath Proof Explorer

Theorem htaOLD

Description: Obsolete version of hta as of 22-Jul-2026. (Contributed by NM, 11-Mar-2004) (Revised by Mario Carneiro, 25-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses htaOLD.1 
|- A = { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) }
htaOLD.2 
|- B = ( iota_ z e. A A. w e. A -. w R z )
Assertion htaOLD 
|- ( R We A -> ( ph -> [. B / x ]. ph ) )

Proof

Step Hyp Ref Expression
1 htaOLD.1 
 |-  A = { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) }
2 htaOLD.2 
 |-  B = ( iota_ z e. A A. w e. A -. w R z )
3 19.8a 
 |-  ( ph -> E. x ph )
4 scott0bsOLD 
 |-  ( E. x ph <-> { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } =/= (/) )
5 1 neeq1i 
 |-  ( A =/= (/) <-> { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } =/= (/) )
6 4 5 bitr4i 
 |-  ( E. x ph <-> A =/= (/) )
7 3 6 sylib 
 |-  ( ph -> A =/= (/) )
8 scottexsOLD 
 |-  { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } e. _V
9 1 8 eqeltri 
 |-  A e. _V
10 9 2 htalem 
 |-  ( ( R We A /\ A =/= (/) ) -> B e. A )
11 10 ex 
 |-  ( R We A -> ( A =/= (/) -> B e. A ) )
12 simpl 
 |-  ( ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) -> ph )
13 12 ss2abi 
 |-  { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } C_ { x | ph }
14 1 13 eqsstri 
 |-  A C_ { x | ph }
15 14 sseli 
 |-  ( B e. A -> B e. { x | ph } )
16 df-sbc 
 |-  ( [. B / x ]. ph <-> B e. { x | ph } )
17 15 16 sylibr 
 |-  ( B e. A -> [. B / x ]. ph )
18 7 11 17 syl56 
 |-  ( R We A -> ( ph -> [. B / x ]. ph ) )