| Step | Hyp | Ref | Expression | 
						
							| 1 |  | smfinfmpt.n |  |-  F/ n ph | 
						
							| 2 |  | smfinfmpt.x |  |-  F/ x ph | 
						
							| 3 |  | smfinfmpt.y |  |-  F/ y ph | 
						
							| 4 |  | smfinfmpt.m |  |-  ( ph -> M e. ZZ ) | 
						
							| 5 |  | smfinfmpt.z |  |-  Z = ( ZZ>= ` M ) | 
						
							| 6 |  | smfinfmpt.s |  |-  ( ph -> S e. SAlg ) | 
						
							| 7 |  | smfinfmpt.b |  |-  ( ( ph /\ n e. Z /\ x e. A ) -> B e. V ) | 
						
							| 8 |  | smfinfmpt.f |  |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) ) | 
						
							| 9 |  | smfinfmpt.d |  |-  D = { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } | 
						
							| 10 |  | smfinfmpt.g |  |-  G = ( x e. D |-> inf ( ran ( n e. Z |-> B ) , RR , < ) ) | 
						
							| 11 |  | eqidd |  |-  ( ph -> ( n e. Z |-> ( x e. A |-> B ) ) = ( n e. Z |-> ( x e. A |-> B ) ) ) | 
						
							| 12 | 11 8 | fvmpt2d |  |-  ( ( ph /\ n e. Z ) -> ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = ( x e. A |-> B ) ) | 
						
							| 13 | 12 | dmeqd |  |-  ( ( ph /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = dom ( x e. A |-> B ) ) | 
						
							| 14 |  | nfcv |  |-  F/_ x Z | 
						
							| 15 | 14 | nfcri |  |-  F/ x n e. Z | 
						
							| 16 | 2 15 | nfan |  |-  F/ x ( ph /\ n e. Z ) | 
						
							| 17 |  | eqid |  |-  ( x e. A |-> B ) = ( x e. A |-> B ) | 
						
							| 18 | 7 | 3expa |  |-  ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. V ) | 
						
							| 19 | 16 17 18 | dmmptdf |  |-  ( ( ph /\ n e. Z ) -> dom ( x e. A |-> B ) = A ) | 
						
							| 20 | 13 19 | eqtr2d |  |-  ( ( ph /\ n e. Z ) -> A = dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) | 
						
							| 21 | 1 20 | iineq2d |  |-  ( ph -> |^|_ n e. Z A = |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) | 
						
							| 22 | 2 21 | rabeqd |  |-  ( ph -> { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ B } ) | 
						
							| 23 |  | nfv |  |-  F/ y x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | 
						
							| 24 | 3 23 | nfan |  |-  F/ y ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) | 
						
							| 25 |  | nfii1 |  |-  F/_ n |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | 
						
							| 26 | 25 | nfcri |  |-  F/ n x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | 
						
							| 27 | 1 26 | nfan |  |-  F/ n ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) | 
						
							| 28 |  | simpll |  |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> ph ) | 
						
							| 29 |  | simpr |  |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> n e. Z ) | 
						
							| 30 |  | eliinid |  |-  ( ( x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) /\ n e. Z ) -> x e. dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) | 
						
							| 31 | 30 | adantll |  |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> x e. dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) | 
						
							| 32 | 13 19 | eqtrd |  |-  ( ( ph /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = A ) | 
						
							| 33 | 32 | adantlr |  |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) = A ) | 
						
							| 34 | 31 33 | eleqtrd |  |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> x e. A ) | 
						
							| 35 | 12 | fveq1d |  |-  ( ( ph /\ n e. Z ) -> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) = ( ( x e. A |-> B ) ` x ) ) | 
						
							| 36 | 35 | 3adant3 |  |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) = ( ( x e. A |-> B ) ` x ) ) | 
						
							| 37 |  | simp3 |  |-  ( ( ph /\ n e. Z /\ x e. A ) -> x e. A ) | 
						
							| 38 |  | fvmpt4 |  |-  ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B ) | 
						
							| 39 | 37 7 38 | syl2anc |  |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B ) | 
						
							| 40 | 36 39 | eqtr2d |  |-  ( ( ph /\ n e. Z /\ x e. A ) -> B = ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) | 
						
							| 41 | 40 | breq2d |  |-  ( ( ph /\ n e. Z /\ x e. A ) -> ( y <_ B <-> y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) ) | 
						
							| 42 | 28 29 34 41 | syl3anc |  |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) /\ n e. Z ) -> ( y <_ B <-> y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) ) | 
						
							| 43 | 27 42 | ralbida |  |-  ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) -> ( A. n e. Z y <_ B <-> A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) ) | 
						
							| 44 | 24 43 | rexbid |  |-  ( ( ph /\ x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ) -> ( E. y e. RR A. n e. Z y <_ B <-> E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) ) | 
						
							| 45 | 2 44 | rabbida |  |-  ( ph -> { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ B } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } ) | 
						
							| 46 | 22 45 | eqtrd |  |-  ( ph -> { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } ) | 
						
							| 47 | 9 46 | eqtrid |  |-  ( ph -> D = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } ) | 
						
							| 48 |  | nfcv |  |-  F/_ n RR | 
						
							| 49 |  | nfra1 |  |-  F/ n A. n e. Z y <_ B | 
						
							| 50 | 48 49 | nfrexw |  |-  F/ n E. y e. RR A. n e. Z y <_ B | 
						
							| 51 |  | nfii1 |  |-  F/_ n |^|_ n e. Z A | 
						
							| 52 | 50 51 | nfrabw |  |-  F/_ n { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } | 
						
							| 53 | 9 52 | nfcxfr |  |-  F/_ n D | 
						
							| 54 | 53 | nfcri |  |-  F/ n x e. D | 
						
							| 55 | 1 54 | nfan |  |-  F/ n ( ph /\ x e. D ) | 
						
							| 56 |  | simpll |  |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ph ) | 
						
							| 57 |  | simpr |  |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> n e. Z ) | 
						
							| 58 |  | rabidim1 |  |-  ( x e. { x e. |^|_ n e. Z A | E. y e. RR A. n e. Z y <_ B } -> x e. |^|_ n e. Z A ) | 
						
							| 59 | 58 9 | eleq2s |  |-  ( x e. D -> x e. |^|_ n e. Z A ) | 
						
							| 60 |  | eliinid |  |-  ( ( x e. |^|_ n e. Z A /\ n e. Z ) -> x e. A ) | 
						
							| 61 | 59 60 | sylan |  |-  ( ( x e. D /\ n e. Z ) -> x e. A ) | 
						
							| 62 | 61 | adantll |  |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> x e. A ) | 
						
							| 63 | 56 57 62 40 | syl3anc |  |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> B = ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) | 
						
							| 64 | 55 63 | mpteq2da |  |-  ( ( ph /\ x e. D ) -> ( n e. Z |-> B ) = ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) ) | 
						
							| 65 | 64 | rneqd |  |-  ( ( ph /\ x e. D ) -> ran ( n e. Z |-> B ) = ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) ) | 
						
							| 66 | 65 | infeq1d |  |-  ( ( ph /\ x e. D ) -> inf ( ran ( n e. Z |-> B ) , RR , < ) = inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) | 
						
							| 67 | 2 47 66 | mpteq12da |  |-  ( ph -> ( x e. D |-> inf ( ran ( n e. Z |-> B ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) ) | 
						
							| 68 | 10 67 | eqtrid |  |-  ( ph -> G = ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) ) | 
						
							| 69 |  | nfmpt1 |  |-  F/_ n ( n e. Z |-> ( x e. A |-> B ) ) | 
						
							| 70 |  | nfmpt1 |  |-  F/_ x ( x e. A |-> B ) | 
						
							| 71 | 14 70 | nfmpt |  |-  F/_ x ( n e. Z |-> ( x e. A |-> B ) ) | 
						
							| 72 | 1 8 | fmptd2f |  |-  ( ph -> ( n e. Z |-> ( x e. A |-> B ) ) : Z --> ( SMblFn ` S ) ) | 
						
							| 73 |  | eqid |  |-  { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } = { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } | 
						
							| 74 |  | eqid |  |-  ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) | 
						
							| 75 | 69 71 4 5 6 72 73 74 | smfinf |  |-  ( ph -> ( x e. { x e. |^|_ n e. Z dom ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) | E. y e. RR A. n e. Z y <_ ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) } |-> inf ( ran ( n e. Z |-> ( ( ( n e. Z |-> ( x e. A |-> B ) ) ` n ) ` x ) ) , RR , < ) ) e. ( SMblFn ` S ) ) | 
						
							| 76 | 68 75 | eqeltrd |  |-  ( ph -> G e. ( SMblFn ` S ) ) |