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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑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 biimtrid ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 1 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
90 89 ralrimiva ⊢ ( 𝜑 → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 1 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
91 fvoveq1 ⊢ ( 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) → ( ♯ ‘ ( 𝑚 supp 0 ) ) = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
92 91 eqeq2d ⊢ ( 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) → ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ↔ 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) ) )
93 oveq1 ⊢ ( 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) → ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) )
94 93 eqeq2d ⊢ ( 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) → ( 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ↔ 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
95 92 94 anbi12d ⊢ ( 𝑚 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) → ( ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ↔ ( 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) ∧ 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) )
96 1 2 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 )
97 4 96 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
98 97 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑥 ∈ 𝐼 ) → 0 ∈ 𝐵 )
99 eqid ⊢ ( 𝐵 ↑m 𝐼 ) = ( 𝐵 ↑m 𝐼 )
100 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) )
101 100 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) )
102 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
103 99 101 102 mapfvd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑙 ‘ 𝑥 ) ∈ 𝐵 )
104 98 103 ifcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑥 ∈ 𝐼 ) → if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ∈ 𝐵 )
105 104 fmpttd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) : 𝐼 ⟶ 𝐵 )
106 9 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 𝐵 ∈ V )
107 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 𝐼 ∈ 𝑉 )
108 106 107 elmapd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∈ ( 𝐵 ↑m 𝐼 ) ↔ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) : 𝐼 ⟶ 𝐵 ) )
109 105 108 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∈ ( 𝐵 ↑m 𝐼 ) )
110 109 adantrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∈ ( 𝐵 ↑m 𝐼 ) )
111 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑙 supp 0 ) ∈ V )
112 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑧 ∈ 𝐼 )
113 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑙 ‘ 𝑧 ) ≠ 0 )
114 elmapfn ⊢ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑙 Fn 𝐼 )
115 114 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 𝑙 Fn 𝐼 )
116 115 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑙 Fn 𝐼 )
117 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝐼 ∈ 𝑉 )
118 33 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 0 ∈ V )
119 elsuppfn ⊢ ( ( 𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑧 ∈ ( 𝑙 supp 0 ) ↔ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) )
120 116 117 118 119 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑧 ∈ ( 𝑙 supp 0 ) ↔ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) )
121 112 113 120 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑧 ∈ ( 𝑙 supp 0 ) )
122 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑗 ∈ ℕ )
123 122 nnnn0d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑗 ∈ ℕ0 )
124 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) )
125 124 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( ♯ ‘ ( 𝑙 supp 0 ) ) = ( 𝑗 + 1 ) )
126 hashdifsnp1 ⊢ ( ( ( 𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ ( 𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑙 supp 0 ) ) = ( 𝑗 + 1 ) → ( ♯ ‘ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ) = 𝑗 ) )
127 126 imp ⊢ ( ( ( ( 𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ ( 𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( ♯ ‘ ( 𝑙 supp 0 ) ) = ( 𝑗 + 1 ) ) → ( ♯ ‘ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ) = 𝑗 )
128 111 121 123 125 127 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( ♯ ‘ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ) = 𝑗 )
129 eldifsn ⊢ ( 𝑣 ∈ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ↔ ( 𝑣 ∈ ( 𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧 ) )
130 fvex ⊢ ( 𝑙 ‘ 𝑥 ) ∈ V
131 33 130 ifex ⊢ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ∈ V
132 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) )
133 131 132 fnmpti ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) Fn 𝐼
134 133 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) Fn 𝐼 )
135 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 𝐼 ∈ 𝑉 )
136 33 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 0 ∈ V )
137 elsuppfn ⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑣 ∈ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) ≠ 0 ) ) )
138 134 135 136 137 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑣 ∈ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) ≠ 0 ) ) )
139 iftrue ⊢ ( 𝑣 = 𝑧 → if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 )
140 olc ⊢ ( 𝑣 = 𝑧 → ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) )
141 139 140 2thd ⊢ ( 𝑣 = 𝑧 → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 ↔ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ) )
142 iffalse ⊢ ( ¬ 𝑣 = 𝑧 → if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = ( 𝑙 ‘ 𝑣 ) )
143 142 eqeq1d ⊢ ( ¬ 𝑣 = 𝑧 → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 ↔ ( 𝑙 ‘ 𝑣 ) = 0 ) )
144 biorf ⊢ ( ¬ 𝑣 = 𝑧 → ( ( 𝑙 ‘ 𝑣 ) = 0 ↔ ( 𝑣 = 𝑧 ∨ ( 𝑙 ‘ 𝑣 ) = 0 ) ) )
145 orcom ⊢ ( ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ↔ ( 𝑣 = 𝑧 ∨ ( 𝑙 ‘ 𝑣 ) = 0 ) )
146 144 145 bitr4di ⊢ ( ¬ 𝑣 = 𝑧 → ( ( 𝑙 ‘ 𝑣 ) = 0 ↔ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ) )
147 143 146 bitrd ⊢ ( ¬ 𝑣 = 𝑧 → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 ↔ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ) )
148 141 147 pm2.61i ⊢ ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 ↔ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) )
149 148 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) = 0 ↔ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ) )
150 149 necon3abid ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ↔ ¬ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) ) )
151 neanior ⊢ ( ( ( 𝑙 ‘ 𝑣 ) ≠ 0 ∧ 𝑣 ≠ 𝑧 ) ↔ ¬ ( ( 𝑙 ‘ 𝑣 ) = 0 ∨ 𝑣 = 𝑧 ) )
152 150 151 bitr4di ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ↔ ( ( 𝑙 ‘ 𝑣 ) ≠ 0 ∧ 𝑣 ≠ 𝑧 ) ) )
153 152 anbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ 𝐼 ∧ if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑙 ‘ 𝑣 ) ≠ 0 ∧ 𝑣 ≠ 𝑧 ) ) ) )
154 anass ⊢ ( ( ( 𝑣 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑣 ) ≠ 0 ) ∧ 𝑣 ≠ 𝑧 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑙 ‘ 𝑣 ) ≠ 0 ∧ 𝑣 ≠ 𝑧 ) ) )
155 153 154 bitr4di ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ 𝐼 ∧ if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ) ↔ ( ( 𝑣 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑣 ) ≠ 0 ) ∧ 𝑣 ≠ 𝑧 ) ) )
156 equequ1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 = 𝑧 ↔ 𝑣 = 𝑧 ) )
157 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝑙 ‘ 𝑥 ) = ( 𝑙 ‘ 𝑣 ) )
158 156 157 ifbieq2d ⊢ ( 𝑥 = 𝑣 → if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) = if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) )
159 158 132 131 fvmpt3i ⊢ ( 𝑣 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) = if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) )
160 159 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) = if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) )
161 160 neeq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) ≠ 0 ↔ if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ) )
162 161 pm5.32da ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) ≠ 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) ≠ 0 ) ) )
163 115 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 𝑙 Fn 𝐼 )
164 elsuppfn ⊢ ( ( 𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑣 ∈ ( 𝑙 supp 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑣 ) ≠ 0 ) ) )
165 163 135 136 164 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑣 ∈ ( 𝑙 supp 0 ) ↔ ( 𝑣 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑣 ) ≠ 0 ) ) )
166 165 anbi1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ ( 𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧 ) ↔ ( ( 𝑣 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑣 ) ≠ 0 ) ∧ 𝑣 ≠ 𝑧 ) ) )
167 155 162 166 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ 𝐼 ∧ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ‘ 𝑣 ) ≠ 0 ) ↔ ( 𝑣 ∈ ( 𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧 ) ) )
168 138 167 bitr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑣 ∈ ( 𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧 ) ↔ 𝑣 ∈ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
169 129 168 bitrid ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑣 ∈ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ↔ 𝑣 ∈ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
170 169 eqrdv ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) )
171 170 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ♯ ‘ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ) = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
172 171 adantrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( ♯ ‘ ( ( 𝑙 supp 0 ) ∖ { 𝑧 } ) ) = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
173 128 172 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) )
174 130 33 ifex ⊢ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ∈ V
175 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) )
176 174 175 fnmpti ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) Fn 𝐼
177 176 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) Fn 𝐼 )
178 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
179 134 177 135 135 178 offn ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) Fn 𝐼 )
180 156 157 ifbieq1d ⊢ ( 𝑥 = 𝑣 → if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) )
181 180 175 174 fvmpt3i ⊢ ( 𝑣 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ‘ 𝑣 ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) )
182 181 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ‘ 𝑣 ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) )
183 134 177 135 135 178 160 182 ofval ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑣 ) = ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) + if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) ) )
184 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → 𝐺 ∈ Grp )
185 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( ( 𝑙 ‘ 𝑧 ) ≠ 0 ∧ 𝑣 ∈ 𝐼 ) ) → 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) )
186 185 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) )
187 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → 𝑣 ∈ 𝐼 )
188 99 186 187 mapfvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝑙 ‘ 𝑣 ) ∈ 𝐵 )
189 1 3 2 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑙 ‘ 𝑣 ) ∈ 𝐵 ) → ( 0 + ( 𝑙 ‘ 𝑣 ) ) = ( 𝑙 ‘ 𝑣 ) )
190 1 3 2 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑙 ‘ 𝑣 ) ∈ 𝐵 ) → ( ( 𝑙 ‘ 𝑣 ) + 0 ) = ( 𝑙 ‘ 𝑣 ) )
191 189 190 ifeq12d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑙 ‘ 𝑣 ) ∈ 𝐵 ) → if ( 𝑣 = 𝑧 , ( 0 + ( 𝑙 ‘ 𝑣 ) ) , ( ( 𝑙 ‘ 𝑣 ) + 0 ) ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , ( 𝑙 ‘ 𝑣 ) ) )
192 184 188 191 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → if ( 𝑣 = 𝑧 , ( 0 + ( 𝑙 ‘ 𝑣 ) ) , ( ( 𝑙 ‘ 𝑣 ) + 0 ) ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , ( 𝑙 ‘ 𝑣 ) ) )
193 ovif12 ⊢ ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) + if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) ) = if ( 𝑣 = 𝑧 , ( 0 + ( 𝑙 ‘ 𝑣 ) ) , ( ( 𝑙 ‘ 𝑣 ) + 0 ) )
194 ifid ⊢ if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , ( 𝑙 ‘ 𝑣 ) ) = ( 𝑙 ‘ 𝑣 )
195 194 eqcomi ⊢ ( 𝑙 ‘ 𝑣 ) = if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , ( 𝑙 ‘ 𝑣 ) )
196 192 193 195 3eqtr4g ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( if ( 𝑣 = 𝑧 , 0 , ( 𝑙 ‘ 𝑣 ) ) + if ( 𝑣 = 𝑧 , ( 𝑙 ‘ 𝑣 ) , 0 ) ) = ( 𝑙 ‘ 𝑣 ) )
197 183 196 eqtr2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝑙 ‘ 𝑣 ) = ( ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ‘ 𝑣 ) )
198 163 179 197 eqfnfvd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) → 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) )
199 198 adantrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) )
200 173 199 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) ∧ 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
201 200 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ( 𝑗 = ( ♯ ‘ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) supp 0 ) ) ∧ 𝑙 = ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 0 , ( 𝑙 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
202 95 110 201 rspcedvdw ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ≠ 0 ) ) → ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
203 114 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 𝑙 Fn 𝐼 )
204 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 𝐼 ∈ 𝑉 )
205 33 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 0 ∈ V )
206 suppvalfn ⊢ ( ( 𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝑙 supp 0 ) = { 𝑧 ∈ 𝐼 ∣ ( 𝑙 ‘ 𝑧 ) ≠ 0 } )
207 203 204 205 206 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( 𝑙 supp 0 ) = { 𝑧 ∈ 𝐼 ∣ ( 𝑙 ‘ 𝑧 ) ≠ 0 } )
208 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) )
209 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
210 209 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( 𝑗 + 1 ) ∈ ℕ )
211 210 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( 𝑗 + 1 ) ≠ 0 )
212 208 211 eqnetrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( ♯ ‘ ( 𝑙 supp 0 ) ) ≠ 0 )
213 ovex ⊢ ( 𝑙 supp 0 ) ∈ V
214 hasheq0 ⊢ ( ( 𝑙 supp 0 ) ∈ V → ( ( ♯ ‘ ( 𝑙 supp 0 ) ) = 0 ↔ ( 𝑙 supp 0 ) = ∅ ) )
215 214 necon3bid ⊢ ( ( 𝑙 supp 0 ) ∈ V → ( ( ♯ ‘ ( 𝑙 supp 0 ) ) ≠ 0 ↔ ( 𝑙 supp 0 ) ≠ ∅ ) )
216 213 215 mp1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( ( ♯ ‘ ( 𝑙 supp 0 ) ) ≠ 0 ↔ ( 𝑙 supp 0 ) ≠ ∅ ) )
217 212 216 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( 𝑙 supp 0 ) ≠ ∅ )
218 207 217 eqnetrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → { 𝑧 ∈ 𝐼 ∣ ( 𝑙 ‘ 𝑧 ) ≠ 0 } ≠ ∅ )
219 rabn0 ⊢ ( { 𝑧 ∈ 𝐼 ∣ ( 𝑙 ‘ 𝑧 ) ≠ 0 } ≠ ∅ ↔ ∃ 𝑧 ∈ 𝐼 ( 𝑙 ‘ 𝑧 ) ≠ 0 )
220 218 219 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ∃ 𝑧 ∈ 𝐼 ( 𝑙 ‘ 𝑧 ) ≠ 0 )
221 202 220 reximddv ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ∃ 𝑧 ∈ 𝐼 ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
222 rexcom ⊢ ( ∃ 𝑧 ∈ 𝐼 ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ↔ ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∃ 𝑧 ∈ 𝐼 ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
223 221 222 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∃ 𝑧 ∈ 𝐼 ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) )
224 simprr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) )
225 fvoveq1 ⊢ ( ℎ = 𝑚 → ( ♯ ‘ ( ℎ supp 0 ) ) = ( ♯ ‘ ( 𝑚 supp 0 ) ) )
226 225 eqeq2d ⊢ ( ℎ = 𝑚 → ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) ↔ 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ) )
227 eleq1w ⊢ ( ℎ = 𝑚 → ( ℎ ∈ 𝐻 ↔ 𝑚 ∈ 𝐻 ) )
228 226 227 imbi12d ⊢ ( ℎ = 𝑚 → ( ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) → 𝑚 ∈ 𝐻 ) ) )
229 228 rspccva ⊢ ( ( ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ∧ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) → 𝑚 ∈ 𝐻 ) )
230 229 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) → 𝑚 ∈ 𝐻 ) )
231 230 imp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ) → 𝑚 ∈ 𝐻 )
232 231 adantllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ) → 𝑚 ∈ 𝐻 )
233 232 adantlrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ) → 𝑚 ∈ 𝐻 )
234 233 adantrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → 𝑚 ∈ 𝐻 )
235 simplrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → 𝑧 ∈ 𝐼 )
236 100 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) )
237 99 236 235 mapfvd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → ( 𝑙 ‘ 𝑧 ) ∈ 𝐵 )
238 72 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐵 ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 )
239 equequ2 ⊢ ( 𝑎 = 𝑧 → ( 𝑥 = 𝑎 ↔ 𝑥 = 𝑧 ) )
240 239 ifbid ⊢ ( 𝑎 = 𝑧 → if ( 𝑥 = 𝑎 , 𝑏 , 0 ) = if ( 𝑥 = 𝑧 , 𝑏 , 0 ) )
241 240 mpteq2dv ⊢ ( 𝑎 = 𝑧 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 𝑏 , 0 ) ) )
242 241 eleq1d ⊢ ( 𝑎 = 𝑧 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 ↔ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 𝑏 , 0 ) ) ∈ 𝐻 ) )
243 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑙 ‘ 𝑥 ) = ( 𝑙 ‘ 𝑧 ) )
244 243 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑏 = ( 𝑙 ‘ 𝑥 ) ↔ 𝑏 = ( 𝑙 ‘ 𝑧 ) ) )
245 244 biimparc ⊢ ( ( 𝑏 = ( 𝑙 ‘ 𝑧 ) ∧ 𝑥 = 𝑧 ) → 𝑏 = ( 𝑙 ‘ 𝑥 ) )
246 245 ifeq1da ⊢ ( 𝑏 = ( 𝑙 ‘ 𝑧 ) → if ( 𝑥 = 𝑧 , 𝑏 , 0 ) = if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) )
247 246 mpteq2dv ⊢ ( 𝑏 = ( 𝑙 ‘ 𝑧 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 𝑏 , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) )
248 247 eleq1d ⊢ ( 𝑏 = ( 𝑙 ‘ 𝑧 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , 𝑏 , 0 ) ) ∈ 𝐻 ↔ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) )
249 242 248 rspc2va ⊢ ( ( ( 𝑧 ∈ 𝐼 ∧ ( 𝑙 ‘ 𝑧 ) ∈ 𝐵 ) ∧ ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐵 ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐻 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 )
250 235 237 238 249 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 )
251 8 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 ∘f + 𝑦 ) ∈ 𝐻 )
252 251 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 ∘f + 𝑦 ) ∈ 𝐻 )
253 ovrspc2v ⊢ ( ( ( 𝑚 ∈ 𝐻 ∧ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ∈ 𝐻 ) ∧ ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 ∘f + 𝑦 ) ∈ 𝐻 ) → ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐻 )
254 234 250 252 253 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ∈ 𝐻 )
255 224 254 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) ∧ ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) ) → 𝑙 ∈ 𝐻 )
256 255 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) ∧ ( 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑧 ∈ 𝐼 ) ) → ( ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) → 𝑙 ∈ 𝐻 ) )
257 256 rexlimdvva ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → ( ∃ 𝑚 ∈ ( 𝐵 ↑m 𝐼 ) ∃ 𝑧 ∈ 𝐼 ( 𝑗 = ( ♯ ‘ ( 𝑚 supp 0 ) ) ∧ 𝑙 = ( 𝑚 ∘f + ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑧 , ( 𝑙 ‘ 𝑥 ) , 0 ) ) ) ) → 𝑙 ∈ 𝐻 ) )
258 223 257 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) ∧ ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ) ) → 𝑙 ∈ 𝐻 )
259 258 exp32 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) → ( 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) → ( ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) → 𝑙 ∈ 𝐻 ) ) )
260 259 ralrimiv ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) → ∀ 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ( ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) → 𝑙 ∈ 𝐻 ) )
261 fvoveq1 ⊢ ( 𝑙 = ℎ → ( ♯ ‘ ( 𝑙 supp 0 ) ) = ( ♯ ‘ ( ℎ supp 0 ) ) )
262 261 eqeq2d ⊢ ( 𝑙 = ℎ → ( ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) ↔ ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) ) )
263 eleq1w ⊢ ( 𝑙 = ℎ → ( 𝑙 ∈ 𝐻 ↔ ℎ ∈ 𝐻 ) )
264 262 263 imbi12d ⊢ ( 𝑙 = ℎ → ( ( ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) → 𝑙 ∈ 𝐻 ) ↔ ( ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) )
265 264 cbvralvw ⊢ ( ∀ 𝑙 ∈ ( 𝐵 ↑m 𝐼 ) ( ( 𝑗 + 1 ) = ( ♯ ‘ ( 𝑙 supp 0 ) ) → 𝑙 ∈ 𝐻 ) ↔ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
266 260 265 sylib ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑗 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ) → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( 𝑗 + 1 ) = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
267 15 18 21 24 90 266 nnindd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
268 267 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
269 ralcom ⊢ ( ∀ 𝑛 ∈ ℕ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ∀ 𝑛 ∈ ℕ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
270 268 269 sylib ⊢ ( 𝜑 → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ∀ 𝑛 ∈ ℕ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) )
271 biidd ⊢ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ( ℎ ∈ 𝐻 ↔ ℎ ∈ 𝐻 ) )
272 271 ceqsralv ⊢ ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ( ∀ 𝑛 ∈ ℕ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) ↔ ℎ ∈ 𝐻 ) )
273 272 biimpcd ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) → ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ℎ ∈ 𝐻 ) )
274 273 ralimi ⊢ ( ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ∀ 𝑛 ∈ ℕ ( 𝑛 = ( ♯ ‘ ( ℎ supp 0 ) ) → ℎ ∈ 𝐻 ) → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ℎ ∈ 𝐻 ) )
275 270 274 syl ⊢ ( 𝜑 → ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ℎ ∈ 𝐻 ) )
276 fvoveq1 ⊢ ( ℎ = 𝑋 → ( ♯ ‘ ( ℎ supp 0 ) ) = ( ♯ ‘ ( 𝑋 supp 0 ) ) )
277 276 eleq1d ⊢ ( ℎ = 𝑋 → ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ ↔ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) )
278 eleq1 ⊢ ( ℎ = 𝑋 → ( ℎ ∈ 𝐻 ↔ 𝑋 ∈ 𝐻 ) )
279 277 278 imbi12d ⊢ ( ℎ = 𝑋 → ( ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ℎ ∈ 𝐻 ) ↔ ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ → 𝑋 ∈ 𝐻 ) ) )
280 279 rspcv ⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → ( ∀ ℎ ∈ ( 𝐵 ↑m 𝐼 ) ( ( ♯ ‘ ( ℎ supp 0 ) ) ∈ ℕ → ℎ ∈ 𝐻 ) → ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ → 𝑋 ∈ 𝐻 ) ) )
281 275 280 syl5com ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ → 𝑋 ∈ 𝐻 ) ) )
282 281 com23 ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑋 ∈ 𝐻 ) ) )
283 282 imp ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑋 ∈ 𝐻 ) )
284 12 283 sylbird ⊢ ( ( 𝜑 ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) → ( 𝑋 : 𝐼 ⟶ 𝐵 → 𝑋 ∈ 𝐻 ) )
285 284 imp ⊢ ( ( ( 𝜑 ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) → 𝑋 ∈ 𝐻 )
286 285 an32s ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) → 𝑋 ∈ 𝐻 )
287 286 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ) → 𝑋 ∈ 𝐻 )
288 ovex ⊢ ( 𝑋 supp 0 ) ∈ V
289 hasheq0 ⊢ ( ( 𝑋 supp 0 ) ∈ V → ( ( ♯ ‘ ( 𝑋 supp 0 ) ) = 0 ↔ ( 𝑋 supp 0 ) = ∅ ) )
290 288 289 ax-mp ⊢ ( ( ♯ ‘ ( 𝑋 supp 0 ) ) = 0 ↔ ( 𝑋 supp 0 ) = ∅ )
291 ffn ⊢ ( 𝑋 : 𝐼 ⟶ 𝐵 → 𝑋 Fn 𝐼 )
292 291 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼 )
293 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → 𝐼 ∈ 𝑉 )
294 33 a1i ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → 0 ∈ V )
295 fnsuppeq0 ⊢ ( ( 𝑋 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( ( 𝑋 supp 0 ) = ∅ ↔ 𝑋 = ( 𝐼 × { 0 } ) ) )
296 292 293 294 295 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → ( ( 𝑋 supp 0 ) = ∅ ↔ 𝑋 = ( 𝐼 × { 0 } ) ) )
297 296 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) ∧ ( 𝑋 supp 0 ) = ∅ ) → 𝑋 = ( 𝐼 × { 0 } ) )
298 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) ∧ ( 𝑋 supp 0 ) = ∅ ) → ( 𝐼 × { 0 } ) ∈ 𝐻 )
299 297 298 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) ∧ ( 𝑋 supp 0 ) = ∅ ) → 𝑋 ∈ 𝐻 )
300 290 299 sylan2b ⊢ ( ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) ∧ ( ♯ ‘ ( 𝑋 supp 0 ) ) = 0 ) → 𝑋 ∈ 𝐻 )
301 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 )
302 301 fsuppimpd ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → ( 𝑋 supp 0 ) ∈ Fin )
303 hashcl ⊢ ( ( 𝑋 supp 0 ) ∈ Fin → ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ0 )
304 302 303 syl ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ0 )
305 elnn0 ⊢ ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ0 ↔ ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ∨ ( ♯ ‘ ( 𝑋 supp 0 ) ) = 0 ) )
306 304 305 sylib ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → ( ( ♯ ‘ ( 𝑋 supp 0 ) ) ∈ ℕ ∨ ( ♯ ‘ ( 𝑋 supp 0 ) ) = 0 ) )
307 287 300 306 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑋 : 𝐼 ⟶ 𝐵 ) ∧ 𝑋 finSupp 0 ) → 𝑋 ∈ 𝐻 )
308 307 anasss ⊢ ( ( 𝜑 ∧ ( 𝑋 : 𝐼 ⟶ 𝐵 ∧ 𝑋 finSupp 0 ) ) → 𝑋 ∈ 𝐻 )