sticksstones11

Description: Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones11.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
	sticksstones11.2	⊢ ( 𝜑 → 𝐾 = 0 )
	sticksstones11.3	⊢ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) )
	sticksstones11.4	⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) )
	sticksstones11.5	⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
	sticksstones11.6	⊢ 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
Assertion	sticksstones11	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sticksstones11.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
2		sticksstones11.2	⊢ ( 𝜑 → 𝐾 = 0 )
3		sticksstones11.3	⊢ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) )
4		sticksstones11.4	⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) )
5		sticksstones11.5	⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
6		sticksstones11.6	⊢ 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
7		0nn0	⊢ 0 ∈ ℕ₀
8	7	a1i	⊢ ( 𝜑 → 0 ∈ ℕ₀ )
9	2 8	eqeltrd	⊢ ( 𝜑 → 𝐾 ∈ ℕ₀ )
10	1 9 3 5 6	sticksstones8	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
11	1 2 4 5 6	sticksstones9	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
12	5	a1i	⊢ ( 𝜑 → 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
13		nfv	⊢ Ⅎ 𝑢 𝜑
14		nfcv	⊢ Ⅎ 𝑢 { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
15		nfcv	⊢ Ⅎ 𝑢 { { ⟨ 1 , 𝑁 ⟩ } }
16		ffn	⊢ ( 𝑢 : { 1 } ⟶ ℕ₀ → 𝑢 Fn { 1 } )
17	16	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 𝑢 Fn { 1 } )
18		1nn	⊢ 1 ∈ ℕ
19	18	a1i	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 1 ∈ ℕ )
20	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 𝑁 ∈ ℕ₀ )
21		fnsng	⊢ ( ( 1 ∈ ℕ ∧ 𝑁 ∈ ℕ₀ ) → { ⟨ 1 , 𝑁 ⟩ } Fn { 1 } )
22	19 20 21	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → { ⟨ 1 , 𝑁 ⟩ } Fn { 1 } )
23		elsni	⊢ ( 𝑝 ∈ { 1 } → 𝑝 = 1 )
24	23	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) → 𝑝 = 1 )
25		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) ∧ 𝑝 = 1 ) → 𝑝 = 1 )
26	25	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) ∧ 𝑝 = 1 ) → ( 𝑢 ‘ 𝑝 ) = ( 𝑢 ‘ 1 ) )
27		simprl	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 𝑢 : { 1 } ⟶ ℕ₀ )
28		1ex	⊢ 1 ∈ V
29	28	snid	⊢ 1 ∈ { 1 }
30	29	a1i	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 1 ∈ { 1 } )
31	27 30	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → ( 𝑢 ‘ 1 ) ∈ ℕ₀ )
32	31	nn0cnd	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → ( 𝑢 ‘ 1 ) ∈ ℂ )
33		fveq2	⊢ ( 𝑖 = 1 → ( 𝑢 ‘ 𝑖 ) = ( 𝑢 ‘ 1 ) )
34	33	sumsn	⊢ ( ( 1 ∈ ℕ ∧ ( 𝑢 ‘ 1 ) ∈ ℂ ) → Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = ( 𝑢 ‘ 1 ) )
35	19 32 34	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = ( 𝑢 ‘ 1 ) )
36	35	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = ( 𝑢 ‘ 1 ) ) → Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = ( 𝑢 ‘ 1 ) )
37	36	eqcomd	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = ( 𝑢 ‘ 1 ) ) → ( 𝑢 ‘ 1 ) = Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) )
38		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = ( 𝑢 ‘ 1 ) ) → Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 )
39	37 38	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = ( 𝑢 ‘ 1 ) ) → ( 𝑢 ‘ 1 ) = 𝑁 )
40	39	ex	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → ( Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = ( 𝑢 ‘ 1 ) → ( 𝑢 ‘ 1 ) = 𝑁 ) )
41	35 40	mpd	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → ( 𝑢 ‘ 1 ) = 𝑁 )
42	41	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) → ( 𝑢 ‘ 1 ) = 𝑁 )
43	18	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) → 1 ∈ ℕ )
44	20	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) → 𝑁 ∈ ℕ₀ )
45		fvsng	⊢ ( ( 1 ∈ ℕ ∧ 𝑁 ∈ ℕ₀ ) → ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) = 𝑁 )
46	43 44 45	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) → ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) = 𝑁 )
47	46	eqcomd	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) → 𝑁 = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) )
48	42 47	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) → ( 𝑢 ‘ 1 ) = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) )
49	48	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) ∧ 𝑝 = 1 ) → ( 𝑢 ‘ 1 ) = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) )
50	25	eqcomd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) ∧ 𝑝 = 1 ) → 1 = 𝑝 )
51	50	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) ∧ 𝑝 = 1 ) → ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑝 ) )
52	26 49 51	3eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) ∧ 𝑝 = 1 ) → ( 𝑢 ‘ 𝑝 ) = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑝 ) )
53	24 52	mpdan	⊢ ( ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) ∧ 𝑝 ∈ { 1 } ) → ( 𝑢 ‘ 𝑝 ) = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑝 ) )
54	17 22 53	eqfnfvd	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 𝑢 = { ⟨ 1 , 𝑁 ⟩ } )
55		fsng	⊢ ( ( 1 ∈ ℕ ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑢 : { 1 } ⟶ { 𝑁 } ↔ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) )
56	19 20 55	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → ( 𝑢 : { 1 } ⟶ { 𝑁 } ↔ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) )
57	54 56	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 𝑢 : { 1 } ⟶ { 𝑁 } )
58		ssidd	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → { 𝑁 } ⊆ { 𝑁 } )
59		fss	⊢ ( ( 𝑢 : { 1 } ⟶ { 𝑁 } ∧ { 𝑁 } ⊆ { 𝑁 } ) → 𝑢 : { 1 } ⟶ { 𝑁 } )
60	57 58 59	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 𝑢 : { 1 } ⟶ { 𝑁 } )
61	60 58 59	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 𝑢 : { 1 } ⟶ { 𝑁 } )
62	61 56	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 𝑢 = { ⟨ 1 , 𝑁 ⟩ } )
63		vex	⊢ 𝑢 ∈ V
64	63	elsn	⊢ ( 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ↔ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } )
65	62 64	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) → 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } )
66	65	ex	⊢ ( 𝜑 → ( ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) → 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) )
67		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
68		fzsn	⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
69	67 68	syl	⊢ ( 𝜑 → ( 1 ... 1 ) = { 1 } )
70	69	eqcomd	⊢ ( 𝜑 → { 1 } = ( 1 ... 1 ) )
71		1e0p1	⊢ 1 = ( 0 + 1 )
72	71	a1i	⊢ ( 𝜑 → 1 = ( 0 + 1 ) )
73	72	oveq2d	⊢ ( 𝜑 → ( 1 ... 1 ) = ( 1 ... ( 0 + 1 ) ) )
74	70 73	eqtrd	⊢ ( 𝜑 → { 1 } = ( 1 ... ( 0 + 1 ) ) )
75	2	eqcomd	⊢ ( 𝜑 → 0 = 𝐾 )
76	75	oveq1d	⊢ ( 𝜑 → ( 0 + 1 ) = ( 𝐾 + 1 ) )
77	76	oveq2d	⊢ ( 𝜑 → ( 1 ... ( 0 + 1 ) ) = ( 1 ... ( 𝐾 + 1 ) ) )
78	74 77	eqtrd	⊢ ( 𝜑 → { 1 } = ( 1 ... ( 𝐾 + 1 ) ) )
79	78	feq2d	⊢ ( 𝜑 → ( 𝑢 : { 1 } ⟶ ℕ₀ ↔ 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ) )
80	78	sumeq1d	⊢ ( 𝜑 → Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) )
81	80	eqeq1d	⊢ ( 𝜑 → ( Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 ) )
82	79 81	anbi12d	⊢ ( 𝜑 → ( ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ↔ ( 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) )
83	82	imbi1d	⊢ ( 𝜑 → ( ( ( 𝑢 : { 1 } ⟶ ℕ₀ ∧ Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 ) → 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) ↔ ( ( 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 ) → 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) ) )
84	66 83	mpbid	⊢ ( 𝜑 → ( ( 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 ) → 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) )
85		feq1	⊢ ( 𝑔 = 𝑢 → ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ↔ 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ) )
86		simpl	⊢ ( ( 𝑔 = 𝑢 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑔 = 𝑢 )
87	86	fveq1d	⊢ ( ( 𝑔 = 𝑢 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝑔 ‘ 𝑖 ) = ( 𝑢 ‘ 𝑖 ) )
88	87	sumeq2dv	⊢ ( 𝑔 = 𝑢 → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) )
89	88	eqeq1d	⊢ ( 𝑔 = 𝑢 → ( Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 ) )
90	85 89	anbi12d	⊢ ( 𝑔 = 𝑢 → ( ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) ↔ ( 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) )
91	63 90	elab	⊢ ( 𝑢 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 ) )
92	91	a1i	⊢ ( 𝜑 → ( 𝑢 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 ) ) )
93	92	imbi1d	⊢ ( 𝜑 → ( ( 𝑢 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } → 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) ↔ ( ( 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 ) → 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) ) )
94	84 93	mpbird	⊢ ( 𝜑 → ( 𝑢 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } → 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) )
95	94	imp	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ) → 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } )
96	95	ex	⊢ ( 𝜑 → ( 𝑢 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } → 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) )
97	13 14 15 96	ssrd	⊢ ( 𝜑 → { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ⊆ { { ⟨ 1 , 𝑁 ⟩ } } )
98	18	a1i	⊢ ( 𝜑 → 1 ∈ ℕ )
99	98 1 55	syl2anc	⊢ ( 𝜑 → ( 𝑢 : { 1 } ⟶ { 𝑁 } ↔ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) )
100	99	bicomd	⊢ ( 𝜑 → ( 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ↔ 𝑢 : { 1 } ⟶ { 𝑁 } ) )
101	100	biimpd	⊢ ( 𝜑 → ( 𝑢 = { ⟨ 1 , 𝑁 ⟩ } → 𝑢 : { 1 } ⟶ { 𝑁 } ) )
102		elsni	⊢ ( 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } → 𝑢 = { ⟨ 1 , 𝑁 ⟩ } )
103	101 102	impel	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) → 𝑢 : { 1 } ⟶ { 𝑁 } )
104	1	snssd	⊢ ( 𝜑 → { 𝑁 } ⊆ ℕ₀ )
105	104	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) → { 𝑁 } ⊆ ℕ₀ )
106		fss	⊢ ( ( 𝑢 : { 1 } ⟶ { 𝑁 } ∧ { 𝑁 } ⊆ ℕ₀ ) → 𝑢 : { 1 } ⟶ ℕ₀ )
107	103 105 106	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) → 𝑢 : { 1 } ⟶ ℕ₀ )
108	79	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) → ( 𝑢 : { 1 } ⟶ ℕ₀ ↔ 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ) )
109	107 108	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) → 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ )
110	102	adantl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) → 𝑢 = { ⟨ 1 , 𝑁 ⟩ } )
111	78	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → { 1 } = ( 1 ... ( 𝐾 + 1 ) ) )
112	111	eqcomd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → ( 1 ... ( 𝐾 + 1 ) ) = { 1 } )
113	112	sumeq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) )
114	18	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → 1 ∈ ℕ )
115	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → 𝑁 ∈ ℕ₀ )
116	115	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → 𝑁 ∈ ℂ )
117	114 115 45	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) = 𝑁 )
118	117	eqcomd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → 𝑁 = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) )
119	110	3adant3	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → 𝑢 = { ⟨ 1 , 𝑁 ⟩ } )
120	119	fveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → ( 𝑢 ‘ 1 ) = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) )
121	118 120	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → 𝑁 = ( 𝑢 ‘ 1 ) )
122	121	eleq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → ( 𝑁 ∈ ℂ ↔ ( 𝑢 ‘ 1 ) ∈ ℂ ) )
123	116 122	mpbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → ( 𝑢 ‘ 1 ) ∈ ℂ )
124	114 123 34	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = ( 𝑢 ‘ 1 ) )
125	120 117	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → ( 𝑢 ‘ 1 ) = 𝑁 )
126	124 125	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → Σ 𝑖 ∈ { 1 } ( 𝑢 ‘ 𝑖 ) = 𝑁 )
127	113 126	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 )
128	127	3expa	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) ∧ 𝑢 = { ⟨ 1 , 𝑁 ⟩ } ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 )
129	110 128	mpdan	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 )
130	109 129	jca	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) → ( 𝑢 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑢 ‘ 𝑖 ) = 𝑁 ) )
131	130 91	sylibr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) → 𝑢 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
132	131	ex	⊢ ( 𝜑 → ( 𝑢 ∈ { { ⟨ 1 , 𝑁 ⟩ } } → 𝑢 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ) )
133	13 15 14 132	ssrd	⊢ ( 𝜑 → { { ⟨ 1 , 𝑁 ⟩ } } ⊆ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
134	97 133	eqssd	⊢ ( 𝜑 → { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ₀ ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } = { { ⟨ 1 , 𝑁 ⟩ } } )
135	12 134	eqtrd	⊢ ( 𝜑 → 𝐴 = { { ⟨ 1 , 𝑁 ⟩ } } )
136		eqss	⊢ ( 𝐴 = { { ⟨ 1 , 𝑁 ⟩ } } ↔ ( 𝐴 ⊆ { { ⟨ 1 , 𝑁 ⟩ } } ∧ { { ⟨ 1 , 𝑁 ⟩ } } ⊆ 𝐴 ) )
137	136	biimpi	⊢ ( 𝐴 = { { ⟨ 1 , 𝑁 ⟩ } } → ( 𝐴 ⊆ { { ⟨ 1 , 𝑁 ⟩ } } ∧ { { ⟨ 1 , 𝑁 ⟩ } } ⊆ 𝐴 ) )
138	137	simpld	⊢ ( 𝐴 = { { ⟨ 1 , 𝑁 ⟩ } } → 𝐴 ⊆ { { ⟨ 1 , 𝑁 ⟩ } } )
139	135 138	syl	⊢ ( 𝜑 → 𝐴 ⊆ { { ⟨ 1 , 𝑁 ⟩ } } )
140		fss	⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐴 ⊆ { { ⟨ 1 , 𝑁 ⟩ } } ) → 𝐺 : 𝐵 ⟶ { { ⟨ 1 , 𝑁 ⟩ } } )
141	11 139 140	syl2anc	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ { { ⟨ 1 , 𝑁 ⟩ } } )
142	141	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝐺 : 𝐵 ⟶ { { ⟨ 1 , 𝑁 ⟩ } } )
143	10	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑐 ) ∈ 𝐵 )
144		fvconst	⊢ ( ( 𝐺 : 𝐵 ⟶ { { ⟨ 1 , 𝑁 ⟩ } } ∧ ( 𝐹 ‘ 𝑐 ) ∈ 𝐵 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑐 ) ) = { ⟨ 1 , 𝑁 ⟩ } )
145	142 143 144	syl2anc	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑐 ) ) = { ⟨ 1 , 𝑁 ⟩ } )
146	135	eleq2d	⊢ ( 𝜑 → ( 𝑐 ∈ 𝐴 ↔ 𝑐 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) )
147	146	biimpd	⊢ ( 𝜑 → ( 𝑐 ∈ 𝐴 → 𝑐 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ) )
148	147	imp	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ { { ⟨ 1 , 𝑁 ⟩ } } )
149		vex	⊢ 𝑐 ∈ V
150	149	elsn	⊢ ( 𝑐 ∈ { { ⟨ 1 , 𝑁 ⟩ } } ↔ 𝑐 = { ⟨ 1 , 𝑁 ⟩ } )
151	148 150	sylib	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 = { ⟨ 1 , 𝑁 ⟩ } )
152	151	eqcomd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → { ⟨ 1 , 𝑁 ⟩ } = 𝑐 )
153	145 152	eqtrd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑐 ) ) = 𝑐 )
154	153	ralrimiva	⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( 𝐺 ‘ ( 𝐹 ‘ 𝑐 ) ) = 𝑐 )
155		simpr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 ∈ 𝐵 )
156		nfv	⊢ Ⅎ 𝑑 𝜑
157		nfcv	⊢ Ⅎ 𝑑 𝐵
158		nfcv	⊢ Ⅎ 𝑑 { ∅ }
159	6	a1i	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
160	159	eleq2d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑑 ∈ 𝐵 ↔ 𝑑 ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ) )
161	160	biimpd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑑 ∈ 𝐵 → 𝑑 ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ) )
162	161	syldbl2	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
163		vex	⊢ 𝑑 ∈ V
164		feq1	⊢ ( 𝑓 = 𝑑 → ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ↔ 𝑑 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ) )
165		fveq1	⊢ ( 𝑓 = 𝑑 → ( 𝑓 ‘ 𝑥 ) = ( 𝑑 ‘ 𝑥 ) )
166		fveq1	⊢ ( 𝑓 = 𝑑 → ( 𝑓 ‘ 𝑦 ) = ( 𝑑 ‘ 𝑦 ) )
167	165 166	breq12d	⊢ ( 𝑓 = 𝑑 → ( ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑑 ‘ 𝑥 ) < ( 𝑑 ‘ 𝑦 ) ) )
168	167	imbi2d	⊢ ( 𝑓 = 𝑑 → ( ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑦 → ( 𝑑 ‘ 𝑥 ) < ( 𝑑 ‘ 𝑦 ) ) ) )
169	168	2ralbidv	⊢ ( 𝑓 = 𝑑 → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑑 ‘ 𝑥 ) < ( 𝑑 ‘ 𝑦 ) ) ) )
170	164 169	anbi12d	⊢ ( 𝑓 = 𝑑 → ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑑 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑑 ‘ 𝑥 ) < ( 𝑑 ‘ 𝑦 ) ) ) ) )
171	163 170	elab	⊢ ( 𝑑 ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( 𝑑 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑑 ‘ 𝑥 ) < ( 𝑑 ‘ 𝑦 ) ) ) )
172	162 171	sylib	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑑 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑑 ‘ 𝑥 ) < ( 𝑑 ‘ 𝑦 ) ) ) )
173	172	simpld	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
174		0lt1	⊢ 0 < 1
175	174	a1i	⊢ ( 𝜑 → 0 < 1 )
176	2 175	eqbrtrd	⊢ ( 𝜑 → 𝐾 < 1 )
177	9	nn0zd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
178		fzn	⊢ ( ( 1 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 < 1 ↔ ( 1 ... 𝐾 ) = ∅ ) )
179	67 177 178	syl2anc	⊢ ( 𝜑 → ( 𝐾 < 1 ↔ ( 1 ... 𝐾 ) = ∅ ) )
180	176 179	mpbid	⊢ ( 𝜑 → ( 1 ... 𝐾 ) = ∅ )
181	180	feq2d	⊢ ( 𝜑 → ( 𝑑 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ↔ 𝑑 : ∅ ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ) )
182	181	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑑 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ↔ 𝑑 : ∅ ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ) )
183	173 182	mpbid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 : ∅ ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
184		f0bi	⊢ ( 𝑑 : ∅ ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ↔ 𝑑 = ∅ )
185	183 184	sylib	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 = ∅ )
186		velsn	⊢ ( 𝑑 ∈ { ∅ } ↔ 𝑑 = ∅ )
187	185 186	sylibr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 ∈ { ∅ } )
188	187	ex	⊢ ( 𝜑 → ( 𝑑 ∈ 𝐵 → 𝑑 ∈ { ∅ } ) )
189		f0	⊢ ∅ : ∅ ⟶ ( 1 ... ( 𝑁 + 𝐾 ) )
190	189	a1i	⊢ ( 𝜑 → ∅ : ∅ ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
191	180	feq2d	⊢ ( 𝜑 → ( ∅ : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ↔ ∅ : ∅ ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ) )
192	190 191	mpbird	⊢ ( 𝜑 → ∅ : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
193		ral0	⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) )
194	193	a1i	⊢ ( 𝜑 → ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) )
195		biidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) → ( ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) ) )
196	180 195	raleqbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) ) )
197	194 196	mpbird	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) )
198	192 197	jca	⊢ ( 𝜑 → ( ∅ : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) ) )
199		0ex	⊢ ∅ ∈ V
200		feq1	⊢ ( 𝑓 = ∅ → ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ↔ ∅ : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ) )
201		fveq1	⊢ ( 𝑓 = ∅ → ( 𝑓 ‘ 𝑥 ) = ( ∅ ‘ 𝑥 ) )
202		fveq1	⊢ ( 𝑓 = ∅ → ( 𝑓 ‘ 𝑦 ) = ( ∅ ‘ 𝑦 ) )
203	201 202	breq12d	⊢ ( 𝑓 = ∅ → ( ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ↔ ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) )
204	203	imbi2d	⊢ ( 𝑓 = ∅ → ( ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) ) )
205	204	2ralbidv	⊢ ( 𝑓 = ∅ → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) ) )
206	200 205	anbi12d	⊢ ( 𝑓 = ∅ → ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ∅ : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) ) ) )
207	206	elabg	⊢ ( ∅ ∈ V → ( ∅ ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( ∅ : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) ) ) )
208	199 207	ax-mp	⊢ ( ∅ ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( ∅ : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ∅ ‘ 𝑥 ) < ( ∅ ‘ 𝑦 ) ) ) )
209	198 208	sylibr	⊢ ( 𝜑 → ∅ ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
210	6	a1i	⊢ ( 𝜑 → 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
211	209 210	eleqtrrd	⊢ ( 𝜑 → ∅ ∈ 𝐵 )
212	211	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ∅ } ) → ∅ ∈ 𝐵 )
213		elsni	⊢ ( 𝑑 ∈ { ∅ } → 𝑑 = ∅ )
214	213	adantl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ∅ } ) → 𝑑 = ∅ )
215	214	eleq1d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ∅ } ) → ( 𝑑 ∈ 𝐵 ↔ ∅ ∈ 𝐵 ) )
216	212 215	mpbird	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { ∅ } ) → 𝑑 ∈ 𝐵 )
217	216	ex	⊢ ( 𝜑 → ( 𝑑 ∈ { ∅ } → 𝑑 ∈ 𝐵 ) )
218	188 217	impbid	⊢ ( 𝜑 → ( 𝑑 ∈ 𝐵 ↔ 𝑑 ∈ { ∅ } ) )
219	156 157 158 218	eqrd	⊢ ( 𝜑 → 𝐵 = { ∅ } )
220	219	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝐵 = { ∅ } )
221	155 220	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 ∈ { ∅ } )
222	163	elsn	⊢ ( 𝑑 ∈ { ∅ } ↔ 𝑑 = ∅ )
223	221 222	sylib	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 = ∅ )
224	223	fveq2d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑑 ) = ( 𝐺 ‘ ∅ ) )
225	224	fveq2d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑑 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ∅ ) ) )
226	180	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 1 ... 𝐾 ) = ∅ )
227	226	mpteq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) = ( 𝑗 ∈ ∅ ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) )
228		mpt0	⊢ ( 𝑗 ∈ ∅ ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) = ∅
229	228	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ∅ ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) = ∅ )
230	227 229	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) = ∅ )
231		fzfid	⊢ ( 𝜑 → ( 1 ... 𝐾 ) ∈ Fin )
232	231	mptexd	⊢ ( 𝜑 → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ V )
233		elsng	⊢ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ V → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ { ∅ } ↔ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) = ∅ ) )
234	232 233	syl	⊢ ( 𝜑 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ { ∅ } ↔ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) = ∅ ) )
235	234	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ { ∅ } ↔ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) = ∅ ) )
236	230 235	mpbird	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ { ∅ } )
237	236 3	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ { ∅ } )
238	237	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝐹 : 𝐴 ⟶ { ∅ } )
239		ffvelrn	⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ ∅ ∈ 𝐵 ) → ( 𝐺 ‘ ∅ ) ∈ 𝐴 )
240	11 211 239	syl2anc	⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) ∈ 𝐴 )
241	240	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝐺 ‘ ∅ ) ∈ 𝐴 )
242		fvconst	⊢ ( ( 𝐹 : 𝐴 ⟶ { ∅ } ∧ ( 𝐺 ‘ ∅ ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝐺 ‘ ∅ ) ) = ∅ )
243	238 241 242	syl2anc	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ ∅ ) ) = ∅ )
244	225 243	eqtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑑 ) ) = ∅ )
245	223	eqcomd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ∅ = 𝑑 )
246	244 245	eqtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑑 ) ) = 𝑑 )
247	246	ralrimiva	⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑑 ) ) = 𝑑 )
248	10 11 154 247	2fvidf1od	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Metamath Proof Explorer

Theorem sticksstones11

Proof