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 ffvelrnd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑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 uncom ⊢ ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) = ( { 𝐽 } ∪ ( 𝑇 ∖ { 𝐽 } ) )
46 simpl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝐽 ∈ 𝑇 )
47 46 snssd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → { 𝐽 } ⊆ 𝑇 )
48 undif ⊢ ( { 𝐽 } ⊆ 𝑇 ↔ ( { 𝐽 } ∪ ( 𝑇 ∖ { 𝐽 } ) ) = 𝑇 )
49 47 48 sylib ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( { 𝐽 } ∪ ( 𝑇 ∖ { 𝐽 } ) ) = 𝑇 )
50 45 49 eqtrid ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) = 𝑇 )
51 50 feq2d ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ⟶ ( 𝑆 ∪ { 𝑦 } ) ↔ ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ ( 𝑆 ∪ { 𝑦 } ) ) )
52 44 51 mpbid ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ ( 𝑆 ∪ { 𝑦 } ) )
53 ssidd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑆 ⊆ 𝑆 )
54 snssi ⊢ ( 𝑦 ∈ 𝑆 → { 𝑦 } ⊆ 𝑆 )
55 54 ad2antrl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → { 𝑦 } ⊆ 𝑆 )
56 53 55 unssd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑆 ∪ { 𝑦 } ) ⊆ 𝑆 )
57 52 56 fssd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ 𝑆 )
58 elmapex ⊢ ( 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) → ( 𝑆 ∈ V ∧ ( 𝑇 ∖ { 𝐽 } ) ∈ V ) )
59 58 ad2antll ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑆 ∈ V ∧ ( 𝑇 ∖ { 𝐽 } ) ∈ V ) )
60 59 simpld ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑆 ∈ V )
61 ssun1 ⊢ 𝑇 ⊆ ( 𝑇 ∪ { 𝐽 } )
62 undif1 ⊢ ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) = ( 𝑇 ∪ { 𝐽 } )
63 59 simprd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑇 ∖ { 𝐽 } ) ∈ V )
64 snex ⊢ { 𝐽 } ∈ V
65 unexg ⊢ ( ( ( 𝑇 ∖ { 𝐽 } ) ∈ V ∧ { 𝐽 } ∈ V ) → ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ∈ V )
66 63 64 65 sylancl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ∈ V )
67 62 66 eqeltrrid ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑇 ∪ { 𝐽 } ) ∈ V )
68 ssexg ⊢ ( ( 𝑇 ⊆ ( 𝑇 ∪ { 𝐽 } ) ∧ ( 𝑇 ∪ { 𝐽 } ) ∈ V ) → 𝑇 ∈ V )
69 61 67 68 sylancr ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑇 ∈ V )
70 60 69 elmapd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ∈ ( 𝑆 ↑m 𝑇 ) ↔ ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ 𝑆 ) )
71 57 70 mpbird ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ∈ ( 𝑆 ↑m 𝑇 ) )
72 eleq1 ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ↔ ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ∈ ( 𝑆 ↑m 𝑇 ) ) )
73 71 72 syl5ibrcom ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) )
74 73 rexlimdvva ⊢ ( 𝐽 ∈ 𝑇 → ( ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) )
75 33 74 impbid ⊢ ( 𝐽 ∈ 𝑇 → ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ↔ ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ) )
76 1 adantl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ) → ( 𝜑 ↔ 𝜓 ) )
77 4 75 76 ralxpxfr2d ⊢ ( 𝐽 ∈ 𝑇 → ( ∀ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝑆 ∀ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝜓 ) )