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 difexg ⊢ ( 𝑇 ∈ V → ( 𝑇 ∖ { 𝐽 } ) ∈ V )
20 18 19 syl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ( 𝑇 ∖ { 𝐽 } ) ∈ V )
21 17 20 elmapd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ↔ ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) : ( 𝑇 ∖ { 𝐽 } ) ⟶ 𝑆 ) )
22 15 21 mpbird ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) )
23 10 ffnd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → 𝑓 Fn 𝑇 )
24 fnsnsplit ⊢ ( ( 𝑓 Fn 𝑇 ∧ 𝐽 ∈ 𝑇 ) → 𝑓 = ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) )
25 23 11 24 syl2anc ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → 𝑓 = ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) )
26 opeq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝐽 ) → ⟨ 𝐽 , 𝑦 ⟩ = ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ )
27 26 sneqd ⊢ ( 𝑦 = ( 𝑓 ‘ 𝐽 ) → { ⟨ 𝐽 , 𝑦 ⟩ } = { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } )
28 27 uneq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝐽 ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) = ( 𝑔 ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) )
29 28 eqeq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝐽 ) → ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ↔ 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) ) )
30 uneq1 ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) = ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) )
31 30 eqeq2d ⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) → ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) ↔ 𝑓 = ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) ) )
32 29 31 rspc2ev ⊢ ( ( ( 𝑓 ‘ 𝐽 ) ∈ 𝑆 ∧ ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ∧ 𝑓 = ( ( 𝑓 ↾ ( 𝑇 ∖ { 𝐽 } ) ) ∪ { ⟨ 𝐽 , ( 𝑓 ‘ 𝐽 ) ⟩ } ) ) → ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) )
33 12 22 25 32 syl3anc ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) → ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) )
34 33 ex ⊢ ( 𝐽 ∈ 𝑇 → ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) → ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ) )
35 elmapi ⊢ ( 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) → 𝑔 : ( 𝑇 ∖ { 𝐽 } ) ⟶ 𝑆 )
36 35 ad2antll ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑔 : ( 𝑇 ∖ { 𝐽 } ) ⟶ 𝑆 )
37 f1osng ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V ) → { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } –1-1-onto→ { 𝑦 } )
38 f1of ⊢ ( { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } –1-1-onto→ { 𝑦 } → { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } ⟶ { 𝑦 } )
39 37 38 syl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑦 ∈ V ) → { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } ⟶ { 𝑦 } )
40 39 elvd ⊢ ( 𝐽 ∈ 𝑇 → { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } ⟶ { 𝑦 } )
41 40 adantr ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } ⟶ { 𝑦 } )
42 incom ⊢ ( ( 𝑇 ∖ { 𝐽 } ) ∩ { 𝐽 } ) = ( { 𝐽 } ∩ ( 𝑇 ∖ { 𝐽 } ) )
43 disjdif ⊢ ( { 𝐽 } ∩ ( 𝑇 ∖ { 𝐽 } ) ) = ∅
44 42 43 eqtri ⊢ ( ( 𝑇 ∖ { 𝐽 } ) ∩ { 𝐽 } ) = ∅
45 44 a1i ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑇 ∖ { 𝐽 } ) ∩ { 𝐽 } ) = ∅ )
46 fun ⊢ ( ( ( 𝑔 : ( 𝑇 ∖ { 𝐽 } ) ⟶ 𝑆 ∧ { ⟨ 𝐽 , 𝑦 ⟩ } : { 𝐽 } ⟶ { 𝑦 } ) ∧ ( ( 𝑇 ∖ { 𝐽 } ) ∩ { 𝐽 } ) = ∅ ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ⟶ ( 𝑆 ∪ { 𝑦 } ) )
47 36 41 45 46 syl21anc ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ⟶ ( 𝑆 ∪ { 𝑦 } ) )
48 uncom ⊢ ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) = ( { 𝐽 } ∪ ( 𝑇 ∖ { 𝐽 } ) )
49 simpl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝐽 ∈ 𝑇 )
50 49 snssd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → { 𝐽 } ⊆ 𝑇 )
51 undif ⊢ ( { 𝐽 } ⊆ 𝑇 ↔ ( { 𝐽 } ∪ ( 𝑇 ∖ { 𝐽 } ) ) = 𝑇 )
52 50 51 sylib ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( { 𝐽 } ∪ ( 𝑇 ∖ { 𝐽 } ) ) = 𝑇 )
53 48 52 syl5eq ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) = 𝑇 )
54 53 feq2d ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ⟶ ( 𝑆 ∪ { 𝑦 } ) ↔ ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ ( 𝑆 ∪ { 𝑦 } ) ) )
55 47 54 mpbid ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ ( 𝑆 ∪ { 𝑦 } ) )
56 ssidd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑆 ⊆ 𝑆 )
57 snssi ⊢ ( 𝑦 ∈ 𝑆 → { 𝑦 } ⊆ 𝑆 )
58 57 ad2antrl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → { 𝑦 } ⊆ 𝑆 )
59 56 58 unssd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑆 ∪ { 𝑦 } ) ⊆ 𝑆 )
60 55 59 fssd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ 𝑆 )
61 elmapex ⊢ ( 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) → ( 𝑆 ∈ V ∧ ( 𝑇 ∖ { 𝐽 } ) ∈ V ) )
62 61 ad2antll ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑆 ∈ V ∧ ( 𝑇 ∖ { 𝐽 } ) ∈ V ) )
63 62 simpld ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑆 ∈ V )
64 ssun1 ⊢ 𝑇 ⊆ ( 𝑇 ∪ { 𝐽 } )
65 undif1 ⊢ ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) = ( 𝑇 ∪ { 𝐽 } )
66 62 simprd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑇 ∖ { 𝐽 } ) ∈ V )
67 snex ⊢ { 𝐽 } ∈ V
68 unexg ⊢ ( ( ( 𝑇 ∖ { 𝐽 } ) ∈ V ∧ { 𝐽 } ∈ V ) → ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ∈ V )
69 66 67 68 sylancl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑇 ∖ { 𝐽 } ) ∪ { 𝐽 } ) ∈ V )
70 65 69 eqeltrrid ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑇 ∪ { 𝐽 } ) ∈ V )
71 ssexg ⊢ ( ( 𝑇 ⊆ ( 𝑇 ∪ { 𝐽 } ) ∧ ( 𝑇 ∪ { 𝐽 } ) ∈ V ) → 𝑇 ∈ V )
72 64 70 71 sylancr ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → 𝑇 ∈ V )
73 63 72 elmapd ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ∈ ( 𝑆 ↑m 𝑇 ) ↔ ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) : 𝑇 ⟶ 𝑆 ) )
74 60 73 mpbird ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ∈ ( 𝑆 ↑m 𝑇 ) )
75 eleq1 ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ↔ ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ∈ ( 𝑆 ↑m 𝑇 ) ) )
76 74 75 syl5ibrcom ⊢ ( ( 𝐽 ∈ 𝑇 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) ) ) → ( 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) )
77 76 rexlimdvva ⊢ ( 𝐽 ∈ 𝑇 → ( ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) → 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ) )
78 34 77 impbid ⊢ ( 𝐽 ∈ 𝑇 → ( 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) ↔ ∃ 𝑦 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ) )
79 1 adantl ⊢ ( ( 𝐽 ∈ 𝑇 ∧ 𝑓 = ( 𝑔 ∪ { ⟨ 𝐽 , 𝑦 ⟩ } ) ) → ( 𝜑 ↔ 𝜓 ) )
80 4 78 79 ralxpxfr2d ⊢ ( 𝐽 ∈ 𝑇 → ( ∀ 𝑓 ∈ ( 𝑆 ↑m 𝑇 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝑆 ∀ 𝑔 ∈ ( 𝑆 ↑m ( 𝑇 ∖ { 𝐽 } ) ) 𝜓 ) )