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→ ( { 𝐴 } × 𝐵 ) )