This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( ⟨ ( 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→ 𝐵 )