Theorem embedsetcestrclem

Description: Lemma for embedsetcestrc . (Contributed by AV, 31-Mar-2020)

	Ref	Expression
Hypotheses	funcsetcestrc.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	funcsetcestrc.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
	funcsetcestrc.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
	funcsetcestrc.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	funcsetcestrc.o	⊢ ( 𝜑 → ω ∈ 𝑈 )
	funcsetcestrclem3.e	⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
	funcsetcestrclem3.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
Assertion	embedsetcestrclem	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		funcsetcestrc.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
2		funcsetcestrc.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
3		funcsetcestrc.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
4		funcsetcestrc.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
5		funcsetcestrc.o	⊢ ( 𝜑 → ω ∈ 𝑈 )
6		funcsetcestrclem3.e	⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
7		funcsetcestrclem3.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
8	1 2 3 4 5 6 7	funcsetcestrclem3	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )
9	1 2 3	funcsetcestrclem1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑦 ) = { ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ } )
10	9	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑦 ) = { ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ } )
11	1 2 3	funcsetcestrclem1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑧 ) = { ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ } )
12	11	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑧 ) = { ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ } )
13	10 12	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ { ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ } ) )
14		opex	⊢ ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ ∈ V
15		sneqbg	⊢ ( ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ ∈ V → ( { ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ } ↔ ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ ) )
16	14 15	mp1i	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( { ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ } ↔ ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ ) )
17		fvexd	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ V )
18		simpl	⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) → 𝑦 ∈ 𝐶 )
19		opthg	⊢ ( ( ( Base ‘ ndx ) ∈ V ∧ 𝑦 ∈ 𝐶 ) → ( ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ ↔ ( ( Base ‘ ndx ) = ( Base ‘ ndx ) ∧ 𝑦 = 𝑧 ) ) )
20	17 18 19	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ ↔ ( ( Base ‘ ndx ) = ( Base ‘ ndx ) ∧ 𝑦 = 𝑧 ) ) )
21		simpr	⊢ ( ( ( Base ‘ ndx ) = ( Base ‘ ndx ) ∧ 𝑦 = 𝑧 ) → 𝑦 = 𝑧 )
22	20 21	syl6bi	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ → 𝑦 = 𝑧 ) )
23	16 22	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( { ⟨ ( Base ‘ ndx ) , 𝑦 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑧 ⟩ } → 𝑦 = 𝑧 ) )
24	13 23	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
25	24	ralrimivva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐶 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
26		dff13	⊢ ( 𝐹 : 𝐶 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐶 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
27	8 25 26	sylanbrc	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1→ 𝐵 )