Metamath Proof Explorer

Theorem psrbagleclOLD

Description: Obsolete version of psrbaglecl as of 5-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrbagleclOLD 
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G e. D )

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 simpr2 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G : I --> NN0 )
3 simpr1 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> F e. D )
4 1 psrbag 
 |-  ( I e. V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
5 4 adantr 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
6 3 5 mpbid 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) )
7 6 simprd 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' F " NN ) e. Fin )
8 1 psrbaglesuppOLD 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' G " NN ) C_ ( `' F " NN ) )
9 7 8 ssfid 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' G " NN ) e. Fin )
10 1 psrbag 
 |-  ( I e. V -> ( G e. D <-> ( G : I --> NN0 /\ ( `' G " NN ) e. Fin ) ) )
11 10 adantr 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( G e. D <-> ( G : I --> NN0 /\ ( `' G " NN ) e. Fin ) ) )
12 2 9 11 mpbir2and 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G e. D )