Metamath Proof Explorer

Theorem fsuppind

Description: Induction on functions F : A --> B with finite support, or in other words the base set of the free module (see frlmelbas and frlmplusgval ). This theorem is structurally general for polynomial proof usage (see mplelbas and mpladd ). Note that hypothesis 0 is redundant when I is nonempty. (Contributed by SN, 18-May-2024)

Ref Expression
Hypotheses fsuppind.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
fsuppind.z ⊢ 0 = ( 0g ‘ 𝐺 )
fsuppind.p ⊢ + = ( +g ‘ 𝐺 )
fsuppind.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
fsuppind.v ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
fsuppind.0 ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ 𝐻 )
fsuppind.1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 )
fsuppind.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ∘f + 𝑦 ) ∈ 𝐻 )
Assertion fsuppind ( ( 𝜑 ∧ ( 𝑋 : 𝐼 ⟶ 𝐵 ∧ 𝑋 finSupp 0 ) ) → 𝑋 ∈ 𝐻 )

Proof

Step Hyp Ref Expression
1 fsuppind.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 fsuppind.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 fsuppind.p ⊢ + = ( +g ‘ 𝐺 )
4 fsuppind.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
5 fsuppind.v ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 fsuppind.0 ⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ 𝐻 )
7 fsuppind.1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 )
8 fsuppind.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ∘f + 𝑦 ) ∈ 𝐻 )
9 1 fvexi ⊢ 𝐵 ∈ V
10 9 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
11 10 5 elmapd ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ 𝐵 ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ 𝐵 ) )
13 eqeq1 ⊢ ( 𝑖 = 1 → ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) ↔ 1 = ( ♯ ‘ ( ℎ supp 0 ) ) ) )
14 13 imbi1d ⊢ ( 𝑖 = 1 → ( ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ( 1 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) )
15 14 ralbidv ⊢ ( 𝑖 = 1 → ( ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 1 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) )
16 eqeq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) ↔ 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) ) )
17 16 imbi1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) )
18 17 ralbidv ⊢ ( 𝑖 = 𝑗 → ( ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) )
19 eqeq1 ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) ↔ ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) ) )
20 19 imbi1d ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ( ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) )
21 20 ralbidv ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) )
22 eqeq1 ⊢ ( 𝑖 = 𝑛 → ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) ↔ 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) ) )
23 22 imbi1d ⊢ ( 𝑖 = 𝑛 → ( ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) )
24 23 ralbidv ⊢ ( 𝑖 = 𝑛 → ( ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑖 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) )
25 eqcom ⊢ ( 1 = ( ♯ ‘ ( ℎ supp 0 ) ) ↔ ( ♯ ‘ ( ℎ supp 0 ) ) = 1 )
26 ovex ⊢ ( ℎ supp 0 ) ∈ V
27 euhash1 ⊢ ( ( ℎ supp 0 ) ∈ V → ( ( ♯ ‘ ( ℎ supp 0 ) ) = 1 ↔ ∃! 𝑐 𝑐 ∈ ( ℎ supp 0 ) ) )
28 26 27 ax-mp ⊢ ( ( ♯ ‘ ( ℎ supp 0 ) ) = 1 ↔ ∃! 𝑐 𝑐 ∈ ( ℎ supp 0 ) )
29 25 28 bitri ⊢ ( 1 = ( ♯ ‘ ( ℎ supp 0 ) ) ↔ ∃! 𝑐 𝑐 ∈ ( ℎ supp 0 ) )
30 elmapfn ⊢ ( ℎ ∈ ( 𝐵 ↑m 𝐼 ) → ℎ Fn 𝐼 )
31 30 adantl ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) → ℎ Fn 𝐼 )
32 5 adantr ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝐼 ∈ 𝑉 )
33 2 fvexi ⊢ 0 ∈ V
34 33 a1i ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) → 0 ∈ V )
35 elsuppfn ⊢ ( ( ℎ Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑐 ∈ ( ℎ supp 0 ) ↔ ( 𝑐 ∈ 𝐼 ∧ ( ℎ ‘ 𝑐 ) ≠ 0 ) ) )
36 31 32 34 35 syl3anc ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑐 ∈ ( ℎ supp 0 ) ↔ ( 𝑐 ∈ 𝐼 ∧ ( ℎ ‘ 𝑐 ) ≠ 0 ) ) )
37 36 eubidv ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) → ( ∃! 𝑐 𝑐 ∈ ( ℎ supp 0 ) ↔ ∃! 𝑐 ( 𝑐 ∈ 𝐼 ∧ ( ℎ ‘ 𝑐 ) ≠ 0 ) ) )
38 df-reu ⊢ ( ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ↔ ∃! 𝑐 ( 𝑐 ∈ 𝐼 ∧ ( ℎ ‘ 𝑐 ) ≠ 0 ) )
39 37 38 bitr4di ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) → ( ∃! 𝑐 𝑐 ∈ ( ℎ supp 0 ) ↔ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) )
40 30 ad2antlr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ℎ Fn 𝐼 )
41 fvex ⊢ ( ℎ ‘ 𝑥 ) ∈ V
42 41 33 ifex ⊢ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ∈ V
43 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) )
44 42 43 fnmpti ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) Fn 𝐼
45 44 a1i ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) Fn 𝐼 )
46 eqeq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ↔ 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) )
47 fveq2 ⊢ ( 𝑥 = 𝑣 → ( ℎ ‘ 𝑥 ) = ( ℎ ‘ 𝑣 ) )
48 46 47 ifbieq1d ⊢ ( 𝑥 = 𝑣 → if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) = if ( 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑣 ) , 0 ) )
49 48 43 42 fvmpt3i ⊢ ( 𝑣 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) ‘ 𝑣 ) = if ( 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑣 ) , 0 ) )
50 49 adantl ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) ‘ 𝑣 ) = if ( 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑣 ) , 0 ) )
51 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) ∧ 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) → ( ℎ ‘ 𝑣 ) = ( ℎ ‘ 𝑣 ) )
52 simpr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → 𝑣 ∈ 𝐼 )
53 simplr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 )
54 fveq2 ⊢ ( 𝑐 = 𝑣 → ( ℎ ‘ 𝑐 ) = ( ℎ ‘ 𝑣 ) )
55 54 neeq1d ⊢ ( 𝑐 = 𝑣 → ( ( ℎ ‘ 𝑐 ) ≠ 0 ↔ ( ℎ ‘ 𝑣 ) ≠ 0 ) )
56 55 riota2 ⊢ ( ( 𝑣 ∈ 𝐼 ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ( ( ℎ ‘ 𝑣 ) ≠ 0 ↔ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) = 𝑣 ) )
57 52 53 56 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑣 ) ≠ 0 ↔ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) = 𝑣 ) )
58 necom ⊢ ( 0 ≠ ( ℎ ‘ 𝑣 ) ↔ ( ℎ ‘ 𝑣 ) ≠ 0 )
59 eqcom ⊢ ( 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ↔ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) = 𝑣 )
60 57 58 59 3bitr4g ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( 0 ≠ ( ℎ ‘ 𝑣 ) ↔ 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) )
61 60 biimpd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( 0 ≠ ( ℎ ‘ 𝑣 ) → 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) )
62 61 necon1bd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ¬ 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → 0 = ( ℎ ‘ 𝑣 ) ) )
63 62 imp ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) ∧ ¬ 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) → 0 = ( ℎ ‘ 𝑣 ) )
64 51 63 ifeqda ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → if ( 𝑣 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑣 ) , 0 ) = ( ℎ ‘ 𝑣 ) )
65 50 64 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ℎ ‘ 𝑣 ) = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) ‘ 𝑣 ) )
66 40 45 65 eqfnfvd ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ℎ = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) )
67 riotacl ⊢ ( ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 → ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∈ 𝐼 )
68 67 adantl ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∈ 𝐼 )
69 elmapi ⊢ ( ℎ ∈ ( 𝐵 ↑m 𝐼 ) → ℎ : 𝐼 ⟶ 𝐵 )
70 69 ad2antlr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ℎ : 𝐼 ⟶ 𝐵 )
71 70 68 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ( ℎ ‘ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) ∈ 𝐵 )
72 7 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐵 ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 )
73 72 ad2antrr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐵 ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 )
74 eqeq2 ⊢ ( 𝑎 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ( 𝑥 = 𝑎 ↔ 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) )
75 74 ifbid ⊢ ( 𝑎 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → if ( 𝑥 = 𝑎 , 𝑏 , 0 ) = if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , 𝑏 , 0 ) )
76 75 mpteq2dv ⊢ ( 𝑎 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , 𝑏 , 0 ) ) )
77 76 eleq1d ⊢ ( 𝑎 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 ↔ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , 𝑏 , 0 ) ) ∈ 𝐻 ) )
78 fveq2 ⊢ ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ( ℎ ‘ 𝑥 ) = ( ℎ ‘ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) )
79 78 eqeq2d ⊢ ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ( 𝑏 = ( ℎ ‘ 𝑥 ) ↔ 𝑏 = ( ℎ ‘ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) ) )
80 79 biimparc ⊢ ( ( 𝑏 = ( ℎ ‘ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) ∧ 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) → 𝑏 = ( ℎ ‘ 𝑥 ) )
81 80 ifeq1da ⊢ ( 𝑏 = ( ℎ ‘ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) → if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , 𝑏 , 0 ) = if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) )
82 81 mpteq2dv ⊢ ( 𝑏 = ( ℎ ‘ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , 𝑏 , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) )
83 82 eleq1d ⊢ ( 𝑏 = ( ℎ ‘ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , 𝑏 , 0 ) ) ∈ 𝐻 ↔ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) )
84 77 83 rspc2va ⊢ ( ( ( ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ∈ 𝐼 ∧ ( ℎ ‘ ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) ) ∈ 𝐵 ) ∧ ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐵 ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 )
85 68 71 73 84 syl21anc ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = ( ℩ 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) , ( ℎ ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 )
86 66 85 eqeltrd ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 ) → ℎ ∈ 𝐻 )
87 86 ex ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) → ( ∃! 𝑐 ∈ 𝐼 ( ℎ ‘ 𝑐 ) ≠ 0 → ℎ ∈ 𝐻 ) )
88 39 87 sylbid ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) → ( ∃! 𝑐 𝑐 ∈ ( ℎ supp 0 ) → ℎ ∈ 𝐻 ) )
89 29 88 syl5bi ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 1 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
90 89 ralrimiva ⊢ ( 𝜑 → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 1 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
91 1 2 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
92 4 91 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
93 92 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑥 ∈ 𝐼 ) → 0 ∈ 𝐵 )
94 eqid ⊢ ( 𝐵 ↑m 𝐼 ) = ( 𝐵 ↑m 𝐼 )
95 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) )
96 95 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) )
97 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
98 94 96 97 mapfvd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑙 ‘ 𝑥 ) ∈ 𝐵 )
99 93 98 ifcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑥 ∈ 𝐼 ) → if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ∈ 𝐵 )
100 99 fmpttd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) : 𝐼 ⟶ 𝐵 )
101 9 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 𝐵 ∈ V )
102 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 𝐼 ∈ 𝑉 )
103 101 102 elmapd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∈ ( 𝐵 ↑m 𝐼 ) ↔ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) : 𝐼 ⟶ 𝐵 ) )
104 100 103 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∈ ( 𝐵 ↑m 𝐼 ) )
105 104 adantrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∈ ( 𝐵 ↑m 𝐼 ) )
106 fvoveq1 ⊢ ( 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) → ( ♯ ‘ ( 𝑚 supp 0 ) ) = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
107 106 eqeq2d ⊢ ( 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) → ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ↔ 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) ) )
108 oveq1 ⊢ ( 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) → ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) )
109 108 eqeq2d ⊢ ( 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) → ( 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ↔ 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
110 107 109 anbi12d ⊢ ( 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) → ( ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ↔ ( 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) ∧ 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) )
111 110 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) ∧ 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ) → ( ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ↔ ( 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) ∧ 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) )
112 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑙 supp 0 ) ∈ V )
113 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑧 ∈ 𝐼 )
114 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑙 ‘ 𝑧 ) ≠ 0 )
115 elmapfn ⊢ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑙 Fn 𝐼 )
116 115 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 𝑙 Fn 𝐼 )
117 116 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑙 Fn 𝐼 )
118 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝐼 ∈ 𝑉 )
119 33 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 0 ∈ V )
120 elsuppfn ⊢ ( ( 𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑧 ∈ ( 𝑙 supp 0 ) ↔ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) )
121 117 118 119 120 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑧 ∈ ( 𝑙 supp 0 ) ↔ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) )
122 113 114 121 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑧 ∈ ( 𝑙 supp 0 ) )
123 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑗 ∈ ℕ )
124 123 nnnn0d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑗 ∈ ℕ0 )
125 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) )
126 125 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( ♯ ‘ ( 𝑙 supp 0 ) ) = ( 𝑗 + 1 ) )
127 hashdifsnp1 ⊢ ( ( ( 𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ ( 𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑙 supp 0 ) ) = ( 𝑗 + 1 ) → ( ♯ ‘ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ) = 𝑗 ) )
128 127 imp ⊢ ( ( ( ( 𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ ( 𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( ♯ ‘ ( 𝑙 supp 0 ) ) = ( 𝑗 + 1 ) ) → ( ♯ ‘ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ) = 𝑗 )
129 112 122 124 126 128 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( ♯ ‘ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ) = 𝑗 )
130 eldifsn ⊢ ( 𝑣 ∈ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ↔ ( 𝑣 ∈ ( 𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧 ) )
131 fvex ⊢ ( 𝑙 ‘ 𝑥 ) ∈ V
132 33 131 ifex ⊢ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ∈ V
133 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) )
134 132 133 fnmpti ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) Fn 𝐼
135 134 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) Fn 𝐼 )
136 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 𝐼 ∈ 𝑉 )
137 33 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 0 ∈ V )
138 elsuppfn ⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑣 ∈ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) ≠ 0 ) ) )
139 135 136 137 138 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑣 ∈ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) ≠ 0 ) ) )
140 iftrue ⊢ ( 𝑣 = 𝑧 → if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 )
141 olc ⊢ ( 𝑣 = 𝑧 → ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) )
142 140 141 2thd ⊢ ( 𝑣 = 𝑧 → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 ↔ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ) )
143 iffalse ⊢ ( ¬ 𝑣 = 𝑧 → if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = ( 𝑙 ‘ 𝑣 ) )
144 143 eqeq1d ⊢ ( ¬ 𝑣 = 𝑧 → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 ↔ ( 𝑙 ‘ 𝑣 ) = 0 ) )
145 biorf ⊢ ( ¬ 𝑣 = 𝑧 → ( ( 𝑙 ‘ 𝑣 ) = 0 ↔ ( 𝑣 = 𝑧 ∨ ( 𝑙 ‘ 𝑣 ) = 0 ) ) )
146 orcom ⊢ ( ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ↔ ( 𝑣 = 𝑧 ∨ ( 𝑙 ‘ 𝑣 ) = 0 ) )
147 145 146 bitr4di ⊢ ( ¬ 𝑣 = 𝑧 → ( ( 𝑙 ‘ 𝑣 ) = 0 ↔ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ) )
148 144 147 bitrd ⊢ ( ¬ 𝑣 = 𝑧 → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 ↔ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ) )
149 142 148 pm2.61i ⊢ ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 ↔ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) )
150 149 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 ↔ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ) )
151 150 necon3abid ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ↔ ¬ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ) )
152 neanior ⊢ ( ( ( 𝑙 ‘ 𝑣 ) ≠ 0 ∧ 𝑣 ≠ 𝑧 ) ↔ ¬ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) )
153 151 152 bitr4di ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ↔ ( ( 𝑙 ‘ 𝑣 ) ≠ 0 ∧ 𝑣 ≠ 𝑧 ) ) )
154 153 anbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ 𝐼 ∧ if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑙 ‘ 𝑣 ) ≠ 0 ∧ 𝑣 ≠ 𝑧 ) ) ) )
155 anass ⊢ ( ( ( 𝑣 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑣 ) ≠ 0 ) ∧ 𝑣 ≠ 𝑧 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑙 ‘ 𝑣 ) ≠ 0 ∧ 𝑣 ≠ 𝑧 ) ) )
156 154 155 bitr4di ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ 𝐼 ∧ if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ) ↔ ( ( 𝑣 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑣 ) ≠ 0 ) ∧ 𝑣 ≠ 𝑧 ) ) )
157 equequ1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 = 𝑧 ↔ 𝑣 = 𝑧 ) )
158 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝑙 ‘ 𝑥 ) = ( 𝑙 ‘ 𝑣 ) )
159 157 158 ifbieq2d ⊢ ( 𝑥 = 𝑣 → if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) = if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) )
160 159 133 132 fvmpt3i ⊢ ( 𝑣 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) = if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) )
161 160 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) = if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) )
162 161 neeq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) ≠ 0 ↔ if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ) )
163 162 pm5.32da ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) ≠ 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ) ) )
164 116 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 𝑙 Fn 𝐼 )
165 elsuppfn ⊢ ( ( 𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑣 ∈ ( 𝑙 supp 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑣 ) ≠ 0 ) ) )
166 164 136 137 165 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑣 ∈ ( 𝑙 supp 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑣 ) ≠ 0 ) ) )
167 166 anbi1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ ( 𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧 ) ↔ ( ( 𝑣 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑣 ) ≠ 0 ) ∧ 𝑣 ≠ 𝑧 ) ) )
168 156 163 167 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) ≠ 0 ) ↔ ( 𝑣 ∈ ( 𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧 ) ) )
169 139 168 bitr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ ( 𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧 ) ↔ 𝑣 ∈ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
170 130 169 syl5bb ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑣 ∈ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ↔ 𝑣 ∈ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
171 170 eqrdv ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) )
172 171 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ♯ ‘ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ) = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
173 172 adantrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( ♯ ‘ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ) = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
174 129 173 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
175 131 33 ifex ⊢ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ∈ V
176 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) )
177 175 176 fnmpti ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) Fn 𝐼
178 177 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) Fn 𝐼 )
179 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
180 135 178 136 136 179 offn ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) Fn 𝐼 )
181 157 158 ifbieq1d ⊢ ( 𝑥 = 𝑣 → if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) )
182 181 176 175 fvmpt3i ⊢ ( 𝑣 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ‘ 𝑣 ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) )
183 182 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ‘ 𝑣 ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) )
184 135 178 136 136 179 161 183 ofval ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑣 ) = ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) + if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) ) )
185 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → 𝐺 ∈ Grp )
186 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( ( 𝑙 ‘ 𝑧 ) ≠ 0 ∧ 𝑣 ∈ 𝐼 ) ) → 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) )
187 186 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) )
188 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → 𝑣 ∈ 𝐼 )
189 94 187 188 mapfvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝑙 ‘ 𝑣 ) ∈ 𝐵 )
190 1 3 2 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑙 ‘ 𝑣 ) ∈ 𝐵 ) → ( 0 + ( 𝑙 ‘ 𝑣 ) ) = ( 𝑙 ‘ 𝑣 ) )
191 1 3 2 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑙 ‘ 𝑣 ) ∈ 𝐵 ) → ( ( 𝑙 ‘ 𝑣 ) + 0 ) = ( 𝑙 ‘ 𝑣 ) )
192 190 191 ifeq12d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑙 ‘ 𝑣 ) ∈ 𝐵 ) → if ( 𝑣 = 𝑧 , ( 0 + ( 𝑙 ‘ 𝑣 ) ) , ( ( 𝑙 ‘ 𝑣 ) + 0 ) ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , ( 𝑙 ‘ 𝑣 ) ) )
193 185 189 192 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → if ( 𝑣 = 𝑧 , ( 0 + ( 𝑙 ‘ 𝑣 ) ) , ( ( 𝑙 ‘ 𝑣 ) + 0 ) ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , ( 𝑙 ‘ 𝑣 ) ) )
194 ovif12 ⊢ ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) + if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) ) = if ( 𝑣 = 𝑧 , ( 0 + ( 𝑙 ‘ 𝑣 ) ) , ( ( 𝑙 ‘ 𝑣 ) + 0 ) )
195 ifid ⊢ if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , ( 𝑙 ‘ 𝑣 ) ) = ( 𝑙 ‘ 𝑣 )
196 195 eqcomi ⊢ ( 𝑙 ‘ 𝑣 ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , ( 𝑙 ‘ 𝑣 ) )
197 193 194 196 3eqtr4g ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) + if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) ) = ( 𝑙 ‘ 𝑣 ) )
198 184 197 eqtr2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝑙 ‘ 𝑣 ) = ( ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑣 ) )
199 164 180 198 eqfnfvd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) )
200 199 adantrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) )
201 174 200 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) ∧ 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
202 201 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) ∧ 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
203 105 111 202 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
204 115 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 𝑙 Fn 𝐼 )
205 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 𝐼 ∈ 𝑉 )
206 33 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 0 ∈ V )
207 suppvalfn ⊢ ( ( 𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑙 supp 0 ) = { 𝑧 ∈ 𝐼 ∣ ( 𝑙 ‘ 𝑧 ) ≠ 0 } )
208 204 205 206 207 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( 𝑙 supp 0 ) = { 𝑧 ∈ 𝐼 ∣ ( 𝑙 ‘ 𝑧 ) ≠ 0 } )
209 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) )
210 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
211 210 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( 𝑗 + 1 ) ∈ ℕ )
212 211 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( 𝑗 + 1 ) ≠ 0 )
213 209 212 eqnetrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( ♯ ‘ ( 𝑙 supp 0 ) ) ≠ 0 )
214 ovex ⊢ ( 𝑙 supp 0 ) ∈ V
215 hasheq0 ⊢ ( ( 𝑙 supp 0 ) ∈ V → ( ( ♯ ‘ ( 𝑙 supp 0 ) ) = 0 ↔ ( 𝑙 supp 0 ) = ∅ ) )
216 215 necon3bid ⊢ ( ( 𝑙 supp 0 ) ∈ V → ( ( ♯ ‘ ( 𝑙 supp 0 ) ) ≠ 0 ↔ ( 𝑙 supp 0 ) ≠ ∅ ) )
217 214 216 mp1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( ( ♯ ‘ ( 𝑙 supp 0 ) ) ≠ 0 ↔ ( 𝑙 supp 0 ) ≠ ∅ ) )
218 213 217 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( 𝑙 supp 0 ) ≠ ∅ )
219 208 218 eqnetrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → { 𝑧 ∈ 𝐼 ∣ ( 𝑙 ‘ 𝑧 ) ≠ 0 } ≠ ∅ )
220 rabn0 ⊢ ( { 𝑧 ∈ 𝐼 ∣ ( 𝑙 ‘ 𝑧 ) ≠ 0 } ≠ ∅ ↔ ∃ 𝑧 ∈ 𝐼 ( 𝑙 ‘ 𝑧 ) ≠ 0 )
221 219 220 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ∃ 𝑧 ∈ 𝐼 ( 𝑙 ‘ 𝑧 ) ≠ 0 )
222 203 221 reximddv ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ∃ 𝑧 ∈ 𝐼 ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
223 rexcom ⊢ ( ∃ 𝑧 ∈ 𝐼 ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ↔ ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∃ 𝑧 ∈ 𝐼 ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
224 222 223 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∃ 𝑧 ∈ 𝐼 ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
225 simprr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) )
226 fvoveq1 ⊢ ( ℎ = 𝑚 → ( ♯ ‘ ( ℎ supp 0 ) ) = ( ♯ ‘ ( 𝑚 supp 0 ) ) )
227 226 eqeq2d ⊢ ( ℎ = 𝑚 → ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) ↔ 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ) )
228 eleq1w ⊢ ( ℎ = 𝑚 → ( ℎ ∈ 𝐻 ↔ 𝑚 ∈ 𝐻 ) )
229 227 228 imbi12d ⊢ ( ℎ = 𝑚 → ( ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) → 𝑚 ∈ 𝐻 ) ) )
230 229 rspccva ⊢ ( ( ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ∧ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) → 𝑚 ∈ 𝐻 ) )
231 230 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) → 𝑚 ∈ 𝐻 ) )
232 231 imp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ) → 𝑚 ∈ 𝐻 )
233 232 adantllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ) → 𝑚 ∈ 𝐻 )
234 233 adantlrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ) → 𝑚 ∈ 𝐻 )
235 234 adantrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → 𝑚 ∈ 𝐻 )
236 simplrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → 𝑧 ∈ 𝐼 )
237 95 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) )
238 94 237 236 mapfvd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → ( 𝑙 ‘ 𝑧 ) ∈ 𝐵 )
239 72 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐵 ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 )
240 equequ2 ⊢ ( 𝑎 = 𝑧 → ( 𝑥 = 𝑎 ↔ 𝑥 = 𝑧 ) )
241 240 ifbid ⊢ ( 𝑎 = 𝑧 → if ( 𝑥 = 𝑎 , 𝑏 , 0 ) = if ( 𝑥 = 𝑧 , 𝑏 , 0 ) )
242 241 mpteq2dv ⊢ ( 𝑎 = 𝑧 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 𝑏 , 0 ) ) )
243 242 eleq1d ⊢ ( 𝑎 = 𝑧 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 ↔ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 𝑏 , 0 ) ) ∈ 𝐻 ) )
244 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑙 ‘ 𝑥 ) = ( 𝑙 ‘ 𝑧 ) )
245 244 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑏 = ( 𝑙 ‘ 𝑥 ) ↔ 𝑏 = ( 𝑙 ‘ 𝑧 ) ) )
246 245 biimparc ⊢ ( ( 𝑏 = ( 𝑙 ‘ 𝑧 ) ∧ 𝑥 = 𝑧 ) → 𝑏 = ( 𝑙 ‘ 𝑥 ) )
247 246 ifeq1da ⊢ ( 𝑏 = ( 𝑙 ‘ 𝑧 ) → if ( 𝑥 = 𝑧 , 𝑏 , 0 ) = if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) )
248 247 mpteq2dv ⊢ ( 𝑏 = ( 𝑙 ‘ 𝑧 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 𝑏 , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) )
249 248 eleq1d ⊢ ( 𝑏 = ( 𝑙 ‘ 𝑧 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 𝑏 , 0 ) ) ∈ 𝐻 ↔ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) )
250 243 249 rspc2va ⊢ ( ( ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ∈ 𝐵 ) ∧ ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐵 ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 )
251 236 238 239 250 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 )
252 8 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 ∘f + 𝑦 ) ∈ 𝐻 )
253 252 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 ∘f + 𝑦 ) ∈ 𝐻 )
254 ovrspc2v ⊢ ( ( ( 𝑚 ∈ 𝐻 ∧ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) ∧ ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 ∘f + 𝑦 ) ∈ 𝐻 ) → ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐻 )
255 235 251 253 254 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐻 )
256 225 255 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → 𝑙 ∈ 𝐻 )
257 256 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) → 𝑙 ∈ 𝐻 ) )
258 257 rexlimdvva ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∃ 𝑧 ∈ 𝐼 ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) → 𝑙 ∈ 𝐻 ) )
259 224 258 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 𝑙 ∈ 𝐻 )
260 259 exp32 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) → ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) → ( ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) → 𝑙 ∈ 𝐻 ) ) )
261 260 ralrimiv ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) → ∀ 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ( ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) → 𝑙 ∈ 𝐻 ) )
262 fvoveq1 ⊢ ( 𝑙 = ℎ → ( ♯ ‘ ( 𝑙 supp 0 ) ) = ( ♯ ‘ ( ℎ supp 0 ) ) )
263 262 eqeq2d ⊢ ( 𝑙 = ℎ → ( ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ↔ ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) ) )
264 eleq1w ⊢ ( 𝑙 = ℎ → ( 𝑙 ∈ 𝐻 ↔ ℎ ∈ 𝐻 ) )
265 263 264 imbi12d ⊢ ( 𝑙 = ℎ → ( ( ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) → 𝑙 ∈ 𝐻 ) ↔ ( ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) )
266 265 cbvralvw ⊢ ( ∀ 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ( ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) → 𝑙 ∈ 𝐻 ) ↔ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
267 261 266 sylib ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
268 15 18 21 24 90 267 nnindd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
269 268 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
270 ralcom ⊢ ( ∀ 𝑛 ∈ ℕ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ∀ 𝑛 ∈ ℕ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
271 269 270 sylib ⊢ ( 𝜑 → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ∀ 𝑛 ∈ ℕ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
272 biidd ⊢ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ( ℎ ∈ 𝐻 ↔ ℎ ∈ 𝐻 ) )
273 272 ceqsralv ⊢ ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ( ∀ 𝑛 ∈ ℕ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ℎ ∈ 𝐻 ) )
274 273 biimpcd ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) → ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ℎ ∈ 𝐻 ) )
275 274 ralimi ⊢ ( ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ∀ 𝑛 ∈ ℕ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ℎ ∈ 𝐻 ) )
276 271 275 syl ⊢ ( 𝜑 → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ℎ ∈ 𝐻 ) )
277 fvoveq1 ⊢ ( ℎ = 𝑋 → ( ♯ ‘ ( ℎ supp 0 ) ) = ( ♯ ‘ ( 𝑋 supp 0 ) ) )
278 277 eleq1d ⊢ ( ℎ = 𝑋 → ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ ↔ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) )
279 eleq1 ⊢ ( ℎ = 𝑋 → ( ℎ ∈ 𝐻 ↔ 𝑋 ∈ 𝐻 ) )
280 278 279 imbi12d ⊢ ( ℎ = 𝑋 → ( ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ℎ ∈ 𝐻 ) ↔ ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ → 𝑋 ∈ 𝐻 ) ) )
281 280 rspcv ⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → ( ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ℎ ∈ 𝐻 ) → ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ → 𝑋 ∈ 𝐻 ) ) )
282 276 281 syl5com ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ → 𝑋 ∈ 𝐻 ) ) )
283 282 com23 ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑋 ∈ 𝐻 ) ) )
284 283 imp ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑋 ∈ 𝐻 ) )
285 12 284 sylbird ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) → ( 𝑋 : 𝐼 ⟶ 𝐵 → 𝑋 ∈ 𝐻 ) )
286 285 imp ⊢ ( ( ( 𝜑 ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) → 𝑋 ∈ 𝐻 )
287 286 an32s ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) → 𝑋 ∈ 𝐻 )
288 287 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) → 𝑋 ∈ 𝐻 )
289 ovex ⊢ ( 𝑋 supp 0 ) ∈ V
290 hasheq0 ⊢ ( ( 𝑋 supp 0 ) ∈ V → ( ( ♯ ‘ ( 𝑋 supp 0 ) ) = 0 ↔ ( 𝑋 supp 0 ) = ∅ ) )
291 289 290 ax-mp ⊢ ( ( ♯ ‘ ( 𝑋 supp 0 ) ) = 0 ↔ ( 𝑋 supp 0 ) = ∅ )
292 ffn ⊢ ( 𝑋 : 𝐼 ⟶ 𝐵 → 𝑋 Fn 𝐼 )
293 292 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼 )
294 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → 𝐼 ∈ 𝑉 )
295 33 a1i ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → 0 ∈ V )
296 fnsuppeq0 ⊢ ( ( 𝑋 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( ( 𝑋 supp 0 ) = ∅ ↔ 𝑋 = ( 𝐼 × { 0 } ) ) )
297 293 294 295 296 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → ( ( 𝑋 supp 0 ) = ∅ ↔ 𝑋 = ( 𝐼 × { 0 } ) ) )
298 297 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) ∧ ( 𝑋 supp 0 ) = ∅ ) → 𝑋 = ( 𝐼 × { 0 } ) )
299 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) ∧ ( 𝑋 supp 0 ) = ∅ ) → ( 𝐼 × { 0 } ) ∈ 𝐻 )
300 298 299 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) ∧ ( 𝑋 supp 0 ) = ∅ ) → 𝑋 ∈ 𝐻 )
301 291 300 sylan2b ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) = 0 ) → 𝑋 ∈ 𝐻 )
302 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 )
303 302 fsuppimpd ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → ( 𝑋 supp 0 ) ∈ Fin )
304 hashcl ⊢ ( ( 𝑋 supp 0 ) ∈ Fin → ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ0 )
305 303 304 syl ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ0 )
306 elnn0 ⊢ ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ0 ↔ ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ∨ ( ♯ ‘ ( 𝑋 supp 0 ) ) = 0 ) )
307 305 306 sylib ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ∨ ( ♯ ‘ ( 𝑋 supp 0 ) ) = 0 ) )
308 288 301 307 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → 𝑋 ∈ 𝐻 )
309 308 anasss ⊢ ( ( 𝜑 ∧ ( 𝑋 : 𝐼 ⟶ 𝐵 ∧ 𝑋 finSupp 0 ) ) → 𝑋 ∈ 𝐻 )