| Step | Hyp | Ref | Expression | 
						
							| 1 |  | smfinfmpt.n | ⊢ Ⅎ 𝑛 𝜑 | 
						
							| 2 |  | smfinfmpt.x | ⊢ Ⅎ 𝑥 𝜑 | 
						
							| 3 |  | smfinfmpt.y | ⊢ Ⅎ 𝑦 𝜑 | 
						
							| 4 |  | smfinfmpt.m | ⊢ ( 𝜑  →  𝑀  ∈  ℤ ) | 
						
							| 5 |  | smfinfmpt.z | ⊢ 𝑍  =  ( ℤ≥ ‘ 𝑀 ) | 
						
							| 6 |  | smfinfmpt.s | ⊢ ( 𝜑  →  𝑆  ∈  SAlg ) | 
						
							| 7 |  | smfinfmpt.b | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍  ∧  𝑥  ∈  𝐴 )  →  𝐵  ∈  𝑉 ) | 
						
							| 8 |  | smfinfmpt.f | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍 )  →  ( 𝑥  ∈  𝐴  ↦  𝐵 )  ∈  ( SMblFn ‘ 𝑆 ) ) | 
						
							| 9 |  | smfinfmpt.d | ⊢ 𝐷  =  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 𝐴  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵 } | 
						
							| 10 |  | smfinfmpt.g | ⊢ 𝐺  =  ( 𝑥  ∈  𝐷  ↦  inf ( ran  ( 𝑛  ∈  𝑍  ↦  𝐵 ) ,  ℝ ,   <  ) ) | 
						
							| 11 |  | eqidd | ⊢ ( 𝜑  →  ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) )  =  ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ) | 
						
							| 12 | 11 8 | fvmpt2d | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍 )  →  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  =  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) | 
						
							| 13 | 12 | dmeqd | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍 )  →  dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  =  dom  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) | 
						
							| 14 |  | nfcv | ⊢ Ⅎ 𝑥 𝑍 | 
						
							| 15 | 14 | nfcri | ⊢ Ⅎ 𝑥 𝑛  ∈  𝑍 | 
						
							| 16 | 2 15 | nfan | ⊢ Ⅎ 𝑥 ( 𝜑  ∧  𝑛  ∈  𝑍 ) | 
						
							| 17 |  | eqid | ⊢ ( 𝑥  ∈  𝐴  ↦  𝐵 )  =  ( 𝑥  ∈  𝐴  ↦  𝐵 ) | 
						
							| 18 | 7 | 3expa | ⊢ ( ( ( 𝜑  ∧  𝑛  ∈  𝑍 )  ∧  𝑥  ∈  𝐴 )  →  𝐵  ∈  𝑉 ) | 
						
							| 19 | 16 17 18 | dmmptdf | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍 )  →  dom  ( 𝑥  ∈  𝐴  ↦  𝐵 )  =  𝐴 ) | 
						
							| 20 | 13 19 | eqtr2d | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍 )  →  𝐴  =  dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ) | 
						
							| 21 | 1 20 | iineq2d | ⊢ ( 𝜑  →  ∩  𝑛  ∈  𝑍 𝐴  =  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ) | 
						
							| 22 | 2 21 | rabeqd | ⊢ ( 𝜑  →  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 𝐴  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵 }  =  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵 } ) | 
						
							| 23 |  | nfv | ⊢ Ⅎ 𝑦 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) | 
						
							| 24 | 3 23 | nfan | ⊢ Ⅎ 𝑦 ( 𝜑  ∧  𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ) | 
						
							| 25 |  | nfii1 | ⊢ Ⅎ 𝑛 ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) | 
						
							| 26 | 25 | nfcri | ⊢ Ⅎ 𝑛 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) | 
						
							| 27 | 1 26 | nfan | ⊢ Ⅎ 𝑛 ( 𝜑  ∧  𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ) | 
						
							| 28 |  | simpll | ⊢ ( ( ( 𝜑  ∧  𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) )  ∧  𝑛  ∈  𝑍 )  →  𝜑 ) | 
						
							| 29 |  | simpr | ⊢ ( ( ( 𝜑  ∧  𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) )  ∧  𝑛  ∈  𝑍 )  →  𝑛  ∈  𝑍 ) | 
						
							| 30 |  | eliinid | ⊢ ( ( 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∧  𝑛  ∈  𝑍 )  →  𝑥  ∈  dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ) | 
						
							| 31 | 30 | adantll | ⊢ ( ( ( 𝜑  ∧  𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) )  ∧  𝑛  ∈  𝑍 )  →  𝑥  ∈  dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ) | 
						
							| 32 | 13 19 | eqtrd | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍 )  →  dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  =  𝐴 ) | 
						
							| 33 | 32 | adantlr | ⊢ ( ( ( 𝜑  ∧  𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) )  ∧  𝑛  ∈  𝑍 )  →  dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  =  𝐴 ) | 
						
							| 34 | 31 33 | eleqtrd | ⊢ ( ( ( 𝜑  ∧  𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) )  ∧  𝑛  ∈  𝑍 )  →  𝑥  ∈  𝐴 ) | 
						
							| 35 | 12 | fveq1d | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍 )  →  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 )  =  ( ( 𝑥  ∈  𝐴  ↦  𝐵 ) ‘ 𝑥 ) ) | 
						
							| 36 | 35 | 3adant3 | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍  ∧  𝑥  ∈  𝐴 )  →  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 )  =  ( ( 𝑥  ∈  𝐴  ↦  𝐵 ) ‘ 𝑥 ) ) | 
						
							| 37 |  | simp3 | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍  ∧  𝑥  ∈  𝐴 )  →  𝑥  ∈  𝐴 ) | 
						
							| 38 |  | fvmpt4 | ⊢ ( ( 𝑥  ∈  𝐴  ∧  𝐵  ∈  𝑉 )  →  ( ( 𝑥  ∈  𝐴  ↦  𝐵 ) ‘ 𝑥 )  =  𝐵 ) | 
						
							| 39 | 37 7 38 | syl2anc | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍  ∧  𝑥  ∈  𝐴 )  →  ( ( 𝑥  ∈  𝐴  ↦  𝐵 ) ‘ 𝑥 )  =  𝐵 ) | 
						
							| 40 | 36 39 | eqtr2d | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍  ∧  𝑥  ∈  𝐴 )  →  𝐵  =  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) | 
						
							| 41 | 40 | breq2d | ⊢ ( ( 𝜑  ∧  𝑛  ∈  𝑍  ∧  𝑥  ∈  𝐴 )  →  ( 𝑦  ≤  𝐵  ↔  𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ) | 
						
							| 42 | 28 29 34 41 | syl3anc | ⊢ ( ( ( 𝜑  ∧  𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) )  ∧  𝑛  ∈  𝑍 )  →  ( 𝑦  ≤  𝐵  ↔  𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ) | 
						
							| 43 | 27 42 | ralbida | ⊢ ( ( 𝜑  ∧  𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) )  →  ( ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵  ↔  ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ) | 
						
							| 44 | 24 43 | rexbid | ⊢ ( ( 𝜑  ∧  𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) )  →  ( ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵  ↔  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ) | 
						
							| 45 | 2 44 | rabbida | ⊢ ( 𝜑  →  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵 }  =  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) } ) | 
						
							| 46 | 22 45 | eqtrd | ⊢ ( 𝜑  →  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 𝐴  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵 }  =  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) } ) | 
						
							| 47 | 9 46 | eqtrid | ⊢ ( 𝜑  →  𝐷  =  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) } ) | 
						
							| 48 |  | nfcv | ⊢ Ⅎ 𝑛 ℝ | 
						
							| 49 |  | nfra1 | ⊢ Ⅎ 𝑛 ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵 | 
						
							| 50 | 48 49 | nfrexw | ⊢ Ⅎ 𝑛 ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵 | 
						
							| 51 |  | nfii1 | ⊢ Ⅎ 𝑛 ∩  𝑛  ∈  𝑍 𝐴 | 
						
							| 52 | 50 51 | nfrabw | ⊢ Ⅎ 𝑛 { 𝑥  ∈  ∩  𝑛  ∈  𝑍 𝐴  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵 } | 
						
							| 53 | 9 52 | nfcxfr | ⊢ Ⅎ 𝑛 𝐷 | 
						
							| 54 | 53 | nfcri | ⊢ Ⅎ 𝑛 𝑥  ∈  𝐷 | 
						
							| 55 | 1 54 | nfan | ⊢ Ⅎ 𝑛 ( 𝜑  ∧  𝑥  ∈  𝐷 ) | 
						
							| 56 |  | simpll | ⊢ ( ( ( 𝜑  ∧  𝑥  ∈  𝐷 )  ∧  𝑛  ∈  𝑍 )  →  𝜑 ) | 
						
							| 57 |  | simpr | ⊢ ( ( ( 𝜑  ∧  𝑥  ∈  𝐷 )  ∧  𝑛  ∈  𝑍 )  →  𝑛  ∈  𝑍 ) | 
						
							| 58 |  | rabidim1 | ⊢ ( 𝑥  ∈  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 𝐴  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  𝐵 }  →  𝑥  ∈  ∩  𝑛  ∈  𝑍 𝐴 ) | 
						
							| 59 | 58 9 | eleq2s | ⊢ ( 𝑥  ∈  𝐷  →  𝑥  ∈  ∩  𝑛  ∈  𝑍 𝐴 ) | 
						
							| 60 |  | eliinid | ⊢ ( ( 𝑥  ∈  ∩  𝑛  ∈  𝑍 𝐴  ∧  𝑛  ∈  𝑍 )  →  𝑥  ∈  𝐴 ) | 
						
							| 61 | 59 60 | sylan | ⊢ ( ( 𝑥  ∈  𝐷  ∧  𝑛  ∈  𝑍 )  →  𝑥  ∈  𝐴 ) | 
						
							| 62 | 61 | adantll | ⊢ ( ( ( 𝜑  ∧  𝑥  ∈  𝐷 )  ∧  𝑛  ∈  𝑍 )  →  𝑥  ∈  𝐴 ) | 
						
							| 63 | 56 57 62 40 | syl3anc | ⊢ ( ( ( 𝜑  ∧  𝑥  ∈  𝐷 )  ∧  𝑛  ∈  𝑍 )  →  𝐵  =  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) | 
						
							| 64 | 55 63 | mpteq2da | ⊢ ( ( 𝜑  ∧  𝑥  ∈  𝐷 )  →  ( 𝑛  ∈  𝑍  ↦  𝐵 )  =  ( 𝑛  ∈  𝑍  ↦  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ) | 
						
							| 65 | 64 | rneqd | ⊢ ( ( 𝜑  ∧  𝑥  ∈  𝐷 )  →  ran  ( 𝑛  ∈  𝑍  ↦  𝐵 )  =  ran  ( 𝑛  ∈  𝑍  ↦  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ) | 
						
							| 66 | 65 | infeq1d | ⊢ ( ( 𝜑  ∧  𝑥  ∈  𝐷 )  →  inf ( ran  ( 𝑛  ∈  𝑍  ↦  𝐵 ) ,  ℝ ,   <  )  =  inf ( ran  ( 𝑛  ∈  𝑍  ↦  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ,  ℝ ,   <  ) ) | 
						
							| 67 | 2 47 66 | mpteq12da | ⊢ ( 𝜑  →  ( 𝑥  ∈  𝐷  ↦  inf ( ran  ( 𝑛  ∈  𝑍  ↦  𝐵 ) ,  ℝ ,   <  ) )  =  ( 𝑥  ∈  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) }  ↦  inf ( ran  ( 𝑛  ∈  𝑍  ↦  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ,  ℝ ,   <  ) ) ) | 
						
							| 68 | 10 67 | eqtrid | ⊢ ( 𝜑  →  𝐺  =  ( 𝑥  ∈  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) }  ↦  inf ( ran  ( 𝑛  ∈  𝑍  ↦  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ,  ℝ ,   <  ) ) ) | 
						
							| 69 |  | nfmpt1 | ⊢ Ⅎ 𝑛 ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) | 
						
							| 70 |  | nfmpt1 | ⊢ Ⅎ 𝑥 ( 𝑥  ∈  𝐴  ↦  𝐵 ) | 
						
							| 71 | 14 70 | nfmpt | ⊢ Ⅎ 𝑥 ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) | 
						
							| 72 | 1 8 | fmptd2f | ⊢ ( 𝜑  →  ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) ) | 
						
							| 73 |  | eqid | ⊢ { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) }  =  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) } | 
						
							| 74 |  | eqid | ⊢ ( 𝑥  ∈  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) }  ↦  inf ( ran  ( 𝑛  ∈  𝑍  ↦  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ,  ℝ ,   <  ) )  =  ( 𝑥  ∈  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) }  ↦  inf ( ran  ( 𝑛  ∈  𝑍  ↦  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ,  ℝ ,   <  ) ) | 
						
							| 75 | 69 71 4 5 6 72 73 74 | smfinf | ⊢ ( 𝜑  →  ( 𝑥  ∈  { 𝑥  ∈  ∩  𝑛  ∈  𝑍 dom  ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 )  ∣  ∃ 𝑦  ∈  ℝ ∀ 𝑛  ∈  𝑍 𝑦  ≤  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) }  ↦  inf ( ran  ( 𝑛  ∈  𝑍  ↦  ( ( ( 𝑛  ∈  𝑍  ↦  ( 𝑥  ∈  𝐴  ↦  𝐵 ) ) ‘ 𝑛 ) ‘ 𝑥 ) ) ,  ℝ ,   <  ) )  ∈  ( SMblFn ‘ 𝑆 ) ) | 
						
							| 76 | 68 75 | eqeltrd | ⊢ ( 𝜑  →  𝐺  ∈  ( SMblFn ‘ 𝑆 ) ) |