Metamath Proof Explorer

Theorem ralxpmap

Description: Quantification over functions in terms of quantification over values and punctured functions. (Contributed by Stefan O'Rear, 27-Feb-2015) (Revised by Stefan O'Rear, 5-May-2015)

Ref Expression
Hypothesis ralxpmap.j ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → ( 𝜑 ↔ 𝜓 ) )
Assertion ralxpmap ( 𝐽 ∈ 𝑇 → ( ∀ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝑆 ∀ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝜓 ) )

Proof

Step Hyp Ref Expression
1 ralxpmap.j ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → ( 𝜑 ↔ 𝜓 ) )
2 vex ⊢ 𝑔 ∈ V
3 snex ⊢ { ⟨ 𝐽 , 𝑦 ⟩ } ∈ V
4 2 3 unex ⊢ ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ∈ V
5 simpr ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) )
6 elmapex ⊢ ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) )
7 6 adantl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) )
8 elmapg ⊢ ( ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ↔ 𝑓 : 𝑇 ⟶ 𝑆 ) )
9 7 8 syl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ↔ 𝑓 : 𝑇 ⟶ 𝑆 ) )
10 5 9 mpbid ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → 𝑓 : 𝑇 ⟶ 𝑆 )
11 simpl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → 𝐽 ∈ 𝑇 )
12 10 11 ffvelcdmd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ( 𝑓 ‘ 𝐽 ) ∈ 𝑆 )
13 difss ⊢ ( 𝑇 ∖ { 𝐽 } ) ⊆ 𝑇
14 fssres ⊢ ( ( 𝑓 : 𝑇 ⟶ 𝑆 ∧ ( 𝑇 ∖ { 𝐽 } ) ⊆ 𝑇 ) → ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) : ( 𝑇 ∖ { 𝐽 } ) ⟶ 𝑆 )
15 10 13 14 sylancl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) : ( 𝑇 ∖ { 𝐽 } ) ⟶ 𝑆 )
16 6 simpld ⊢ ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) → 𝑆 ∈ V )
17 16 adantl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → 𝑆 ∈ V )
18 7 simprd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → 𝑇 ∈ V )
19 18 difexd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ( 𝑇 ∖ { 𝐽 } ) ∈ V )
20 17 19 elmapd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ↔ ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) : ( 𝑇 ∖ { 𝐽 } ) ⟶ 𝑆 ) )
21 15 20 mpbird ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) )
22 10 ffnd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → 𝑓 Fn 𝑇 )
23 fnsnsplit ⊢ ( ( 𝑓 Fn 𝑇 ∧ 𝐽 ∈ 𝑇 ) → 𝑓 = ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) )
24 22 11 23 syl2anc ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → 𝑓 = ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) )
25 opeq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝐽 ) → ⟨ 𝐽 , 𝑦 ⟩ = ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ )
26 25 sneqd ⊢ ( 𝑦 = ( 𝑓 ‘ 𝐽 ) → { ⟨ 𝐽 , 𝑦 ⟩ } = { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } )
27 26 uneq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝐽 ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) = ( 𝑔 ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) )
28 27 eqeq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝐽 ) → ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ↔ 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) ) )
29 uneq1 ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) = ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) )
30 29 eqeq2d ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) → ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) ↔ 𝑓 = ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) ) )
31 28 30 rspc2ev ⊢ ( ( ( 𝑓 ‘ 𝐽 ) ∈ 𝑆 ∧ ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ∧ 𝑓 = ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) ) → ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) )
32 12 21 24 31 syl3anc ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) )
33 32 ex ⊢ ( 𝐽 ∈ 𝑇 → ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) → ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ) )
34 elmapi ⊢ ( 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) → 𝑔 : ( 𝑇 ∖ { 𝐽 } ) ⟶ 𝑆 )
35 34 ad2antll ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑔 : ( 𝑇 ∖ { 𝐽 } ) ⟶ 𝑆 )
36 f1osng ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V ) → { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } –1-1-onto→ { 𝑦 } )
37 f1of ⊢ ( { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } –1-1-onto→ { 𝑦 } → { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } ⟶ { 𝑦 } )
38 36 37 syl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V ) → { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } ⟶ { 𝑦 } )
39 38 elvd ⊢ ( 𝐽 ∈ 𝑇 → { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } ⟶ { 𝑦 } )
40 39 adantr ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } ⟶ { 𝑦 } )
41 disjdifr ⊢ ( ( 𝑇 ∖ { 𝐽 } ) ∩ { 𝐽 } ) = ∅
42 41 a1i ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑇 ∖ { 𝐽 } ) ∩ { 𝐽 } ) = ∅ )
43 fun ⊢ ( ( ( 𝑔 : ( 𝑇 ∖ { 𝐽 } ) ⟶ 𝑆 ∧ { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } ⟶ { 𝑦 } ) ∧ ( ( 𝑇 ∖ { 𝐽 } ) ∩ { 𝐽 } ) = ∅ ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ⟶ ( 𝑆 ∪ { 𝑦 } ) )
44 35 40 42 43 syl21anc ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ⟶ ( 𝑆 ∪ { 𝑦 } ) )
45 simpl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝐽 ∈ 𝑇 )
46 45 snssd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → { 𝐽 } ⊆ 𝑇 )
47 undifr ⊢ ( { 𝐽 } ⊆ 𝑇 ↔ ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) = 𝑇 )
48 46 47 sylib ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) = 𝑇 )
49 48 feq2d ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ⟶ ( 𝑆 ∪ { 𝑦 } ) ↔ ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ ( 𝑆 ∪ { 𝑦 } ) ) )
50 44 49 mpbid ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ ( 𝑆 ∪ { 𝑦 } ) )
51 ssidd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑆 ⊆ 𝑆 )
52 snssi ⊢ ( 𝑦 ∈ 𝑆 → { 𝑦 } ⊆ 𝑆 )
53 52 ad2antrl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → { 𝑦 } ⊆ 𝑆 )
54 51 53 unssd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑆 ∪ { 𝑦 } ) ⊆ 𝑆 )
55 50 54 fssd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ 𝑆 )
56 elmapex ⊢ ( 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) → ( 𝑆 ∈ V ∧ ( 𝑇 ∖ { 𝐽 } ) ∈ V ) )
57 56 ad2antll ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑆 ∈ V ∧ ( 𝑇 ∖ { 𝐽 } ) ∈ V ) )
58 57 simpld ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑆 ∈ V )
59 ssun1 ⊢ 𝑇 ⊆ ( 𝑇 ∪ { 𝐽 } )
60 undif1 ⊢ ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) = ( 𝑇 ∪ { 𝐽 } )
61 57 simprd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑇 ∖ { 𝐽 } ) ∈ V )
62 snex ⊢ { 𝐽 } ∈ V
63 unexg ⊢ ( ( ( 𝑇 ∖ { 𝐽 } ) ∈ V ∧ { 𝐽 } ∈ V ) → ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ∈ V )
64 61 62 63 sylancl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ∈ V )
65 60 64 eqeltrrid ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑇 ∪ { 𝐽 } ) ∈ V )
66 ssexg ⊢ ( ( 𝑇 ⊆ ( 𝑇 ∪ { 𝐽 } ) ∧ ( 𝑇 ∪ { 𝐽 } ) ∈ V ) → 𝑇 ∈ V )
67 59 65 66 sylancr ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑇 ∈ V )
68 58 67 elmapd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ∈ ( 𝑆 ↑m 𝑇 ) ↔ ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ 𝑆 ) )
69 55 68 mpbird ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ∈ ( 𝑆 ↑m 𝑇 ) )
70 eleq1 ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ↔ ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ∈ ( 𝑆 ↑m 𝑇 ) ) )
71 69 70 syl5ibrcom ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) )
72 71 rexlimdvva ⊢ ( 𝐽 ∈ 𝑇 → ( ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) )
73 33 72 impbid ⊢ ( 𝐽 ∈ 𝑇 → ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ↔ ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ) )
74 1 adantl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ) → ( 𝜑 ↔ 𝜓 ) )
75 4 73 74 ralxpxfr2d ⊢ ( 𝐽 ∈ 𝑇 → ( ∀ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝑆 ∀ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝜓 ) )