Metamath Proof Explorer

Theorem projf1o

Description: A biijection from a set to a projection in a two dimensional space. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses projf1o.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
projf1o.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ 𝐴 , 𝑥 ⟩ )
Assertion projf1o ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ ( { 𝐴 } × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 projf1o.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 projf1o.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ⟨ 𝐴 , 𝑥 ⟩ )
3 snidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
4 1 3 syl ⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
5 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐴 ∈ { 𝐴 } )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
7 5 6 opelxpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝐴 , 𝑦 ⟩ ∈ ( { 𝐴 } × 𝐵 ) )
8 opeq2 ⊢ ( 𝑥 = 𝑦 → ⟨ 𝐴 , 𝑥 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
9 8 cbvmptv ⊢ ( 𝑥 ∈ 𝐵 ↦ ⟨ 𝐴 , 𝑥 ⟩ ) = ( 𝑦 ∈ 𝐵 ↦ ⟨ 𝐴 , 𝑦 ⟩ )
10 2 9 eqtri ⊢ 𝐹 = ( 𝑦 ∈ 𝐵 ↦ ⟨ 𝐴 , 𝑦 ⟩ )
11 7 10 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( { 𝐴 } × 𝐵 ) )
12 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) → 𝜑 )
13 2 8 6 7 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) = ⟨ 𝐴 , 𝑦 ⟩ )
14 13 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝐴 , 𝑦 ⟩ = ( 𝐹 ‘ 𝑦 ) )
15 14 3adant3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ⟨ 𝐴 , 𝑦 ⟩ = ( 𝐹 ‘ 𝑦 ) )
16 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) → ⟨ 𝐴 , 𝑦 ⟩ = ( 𝐹 ‘ 𝑦 ) )
17 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
18 opeq2 ⊢ ( 𝑦 = 𝑧 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑧 ⟩ )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
20 opex ⊢ ⟨ 𝐴 , 𝑧 ⟩ ∈ V
21 20 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ⟨ 𝐴 , 𝑧 ⟩ ∈ V )
22 10 18 19 21 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = ⟨ 𝐴 , 𝑧 ⟩ )
23 22 3adant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) = ⟨ 𝐴 , 𝑧 ⟩ )
24 23 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) = ⟨ 𝐴 , 𝑧 ⟩ )
25 16 17 24 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑧 ⟩ )
26 vex ⊢ 𝑧 ∈ V
27 26 a1i ⊢ ( 𝜑 → 𝑧 ∈ V )
28 opthg2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑧 ∈ V ) → ( ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑧 ⟩ ↔ ( 𝐴 = 𝐴 ∧ 𝑦 = 𝑧 ) ) )
29 1 27 28 syl2anc ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑧 ⟩ ↔ ( 𝐴 = 𝐴 ∧ 𝑦 = 𝑧 ) ) )
30 29 simplbda ⊢ ( ( 𝜑 ∧ ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑧 ⟩ ) → 𝑦 = 𝑧 )
31 12 25 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) → 𝑦 = 𝑧 )
32 31 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
33 32 3expb ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
34 33 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
35 dff13 ⊢ ( 𝐹 : 𝐵 –1-1→ ( { 𝐴 } × 𝐵 ) ↔ ( 𝐹 : 𝐵 ⟶ ( { 𝐴 } × 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
36 11 34 35 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ ( { 𝐴 } × 𝐵 ) )
37 elsnxp ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑧 ∈ ( { 𝐴 } × 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ ) )
38 1 37 syl ⊢ ( 𝜑 → ( 𝑧 ∈ ( { 𝐴 } × 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ ) )
39 38 biimpa ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝐴 } × 𝐵 ) ) → ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ )
40 13 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑦 ) = ⟨ 𝐴 , 𝑦 ⟩ )
41 id ⊢ ( 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ → 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ )
42 41 eqcomd ⊢ ( 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ → ⟨ 𝐴 , 𝑦 ⟩ = 𝑧 )
43 42 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ ) → ⟨ 𝐴 , 𝑦 ⟩ = 𝑧 )
44 40 43 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ ) → 𝑧 = ( 𝐹 ‘ 𝑦 ) )
45 44 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ → 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝐴 } × 𝐵 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ → 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
47 46 reximdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝐴 } × 𝐵 ) ) → ( ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝐴 , 𝑦 ⟩ → ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
48 39 47 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝐴 } × 𝐵 ) ) → ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝐹 ‘ 𝑦 ) )
49 48 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( { 𝐴 } × 𝐵 ) ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝐹 ‘ 𝑦 ) )
50 dffo3 ⊢ ( 𝐹 : 𝐵 –onto→ ( { 𝐴 } × 𝐵 ) ↔ ( 𝐹 : 𝐵 ⟶ ( { 𝐴 } × 𝐵 ) ∧ ∀ 𝑧 ∈ ( { 𝐴 } × 𝐵 ) ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝐹 ‘ 𝑦 ) ) )
51 11 49 50 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐵 –onto→ ( { 𝐴 } × 𝐵 ) )
52 df-f1o ⊢ ( 𝐹 : 𝐵 –1-1-onto→ ( { 𝐴 } × 𝐵 ) ↔ ( 𝐹 : 𝐵 –1-1→ ( { 𝐴 } × 𝐵 ) ∧ 𝐹 : 𝐵 –onto→ ( { 𝐴 } × 𝐵 ) ) )
53 36 51 52 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ ( { 𝐴 } × 𝐵 ) )