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

Metamath Proof Explorer

Theorem fpropnf1

Description: A function, given by an unordered pair of ordered pairs, which is not injective/one-to-one. (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 8-Jan-2021)

Ref Expression
Hypothesis fpropnf1.f ⊢ 𝐹 = { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ }
Assertion fpropnf1 ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( Fun 𝐹 ∧ ¬ Fun ◡ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 fpropnf1.f ⊢ 𝐹 = { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ }
2 id ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) )
3 2 3adant3 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) )
4 3 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) )
5 id ⊢ ( 𝑍 ∈ 𝑊 → 𝑍 ∈ 𝑊 )
6 5 5 jca ⊢ ( 𝑍 ∈ 𝑊 → ( 𝑍 ∈ 𝑊 ∧ 𝑍 ∈ 𝑊 ) )
7 6 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑍 ∈ 𝑊 ∧ 𝑍 ∈ 𝑊 ) )
8 7 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝑍 ∈ 𝑊 ∧ 𝑍 ∈ 𝑊 ) )
9 simpr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
10 4 8 9 3jca ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑍 ∈ 𝑊 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) )
11 funprg ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑍 ∈ 𝑊 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → Fun { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } )
12 10 11 syl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → Fun { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } )
13 1 funeqi ⊢ ( Fun 𝐹 ↔ Fun { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } )
14 12 13 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → Fun 𝐹 )
15 neneq ⊢ ( 𝑋 ≠ 𝑌 → ¬ 𝑋 = 𝑌 )
16 15 adantl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ¬ 𝑋 = 𝑌 )
17 fprg ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝑍 ∈ 𝑊 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } : { 𝑋 , 𝑌 } ⟶ { 𝑍 , 𝑍 } )
18 10 17 syl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } : { 𝑋 , 𝑌 } ⟶ { 𝑍 , 𝑍 } )
19 1 eqcomi ⊢ { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } = 𝐹
20 19 feq1i ⊢ ( { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } : { 𝑋 , 𝑌 } ⟶ { 𝑍 , 𝑍 } ↔ 𝐹 : { 𝑋 , 𝑌 } ⟶ { 𝑍 , 𝑍 } )
21 18 20 sylib ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → 𝐹 : { 𝑋 , 𝑌 } ⟶ { 𝑍 , 𝑍 } )
22 df-f1 ⊢ ( 𝐹 : { 𝑋 , 𝑌 } –1-1→ { 𝑍 , 𝑍 } ↔ ( 𝐹 : { 𝑋 , 𝑌 } ⟶ { 𝑍 , 𝑍 } ∧ Fun ◡ 𝐹 ) )
23 dff13 ⊢ ( 𝐹 : { 𝑋 , 𝑌 } –1-1→ { 𝑍 , 𝑍 } ↔ ( 𝐹 : { 𝑋 , 𝑌 } ⟶ { 𝑍 , 𝑍 } ∧ ∀ 𝑥 ∈ { 𝑋 , 𝑌 } ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
24 fveqeq2 ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ) )
25 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝑦 ↔ 𝑋 = 𝑦 ) )
26 24 25 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ) )
27 26 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ) )
28 fveqeq2 ⊢ ( 𝑥 = 𝑌 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) ) )
29 eqeq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 = 𝑦 ↔ 𝑌 = 𝑦 ) )
30 28 29 imbi12d ⊢ ( 𝑥 = 𝑌 → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ) )
31 30 ralbidv ⊢ ( 𝑥 = 𝑌 → ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ) )
32 27 31 ralprg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ { 𝑋 , 𝑌 } ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ∧ ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ) ) )
33 32 3adant3 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ { 𝑋 , 𝑌 } ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ∧ ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ) ) )
34 33 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑥 ∈ { 𝑋 , 𝑌 } ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ∧ ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ) ) )
35 fveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
36 35 eqeq2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) ) )
37 eqeq2 ⊢ ( 𝑦 = 𝑋 → ( 𝑋 = 𝑦 ↔ 𝑋 = 𝑋 ) )
38 36 37 imbi12d ⊢ ( 𝑦 = 𝑋 → ( ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 = 𝑋 ) ) )
39 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
40 39 eqeq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )
41 eqeq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 = 𝑦 ↔ 𝑋 = 𝑌 ) )
42 40 41 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )
43 38 42 ralprg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ↔ ( ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ) )
44 35 eqeq2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) ) )
45 eqeq2 ⊢ ( 𝑦 = 𝑋 → ( 𝑌 = 𝑦 ↔ 𝑌 = 𝑋 ) )
46 44 45 imbi12d ⊢ ( 𝑦 = 𝑋 → ( ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) → 𝑌 = 𝑋 ) ) )
47 39 eqeq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) ) )
48 eqeq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑌 = 𝑦 ↔ 𝑌 = 𝑌 ) )
49 47 48 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) → 𝑌 = 𝑌 ) ) )
50 46 49 ralprg ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ↔ ( ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) → 𝑌 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) → 𝑌 = 𝑌 ) ) ) )
51 43 50 anbi12d ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ∧ ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ) ↔ ( ( ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ∧ ( ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) → 𝑌 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) → 𝑌 = 𝑌 ) ) ) ) )
52 51 3adant3 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ∧ ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ) ↔ ( ( ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ∧ ( ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) → 𝑌 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) → 𝑌 = 𝑌 ) ) ) ) )
53 52 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ∧ ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ) ↔ ( ( ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ∧ ( ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) → 𝑌 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) → 𝑌 = 𝑌 ) ) ) ) )
54 1 fveq1i ⊢ ( 𝐹 ‘ 𝑋 ) = ( { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } ‘ 𝑋 )
55 3simpb ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊 ) )
56 55 anim1i ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) )
57 df-3an ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) )
58 56 57 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊 ∧ 𝑋 ≠ 𝑌 ) )
59 fvpr1g ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊 ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } ‘ 𝑋 ) = 𝑍 )
60 58 59 syl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } ‘ 𝑋 ) = 𝑍 )
61 54 60 eqtrid ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 )
62 1 fveq1i ⊢ ( 𝐹 ‘ 𝑌 ) = ( { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } ‘ 𝑌 )
63 3simpc ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) )
64 63 anim1i ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) )
65 df-3an ⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) )
66 64 65 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝑋 ≠ 𝑌 ) )
67 fvpr2g ⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } ‘ 𝑌 ) = 𝑍 )
68 66 67 syl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( { ⟨ 𝑋 , 𝑍 ⟩ , ⟨ 𝑌 , 𝑍 ⟩ } ‘ 𝑌 ) = 𝑍 )
69 62 68 eqtr2id ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → 𝑍 = ( 𝐹 ‘ 𝑌 ) )
70 61 69 eqtrd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
71 idd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 = 𝑌 → 𝑋 = 𝑌 ) )
72 70 71 embantd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) → 𝑋 = 𝑌 ) )
73 72 adantld ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) → 𝑋 = 𝑌 ) )
74 73 adantrd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( ( ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) → 𝑋 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) ∧ ( ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) → 𝑌 = 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) → 𝑌 = 𝑌 ) ) ) → 𝑋 = 𝑌 ) )
75 53 74 sylbid ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ∧ ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑦 ) → 𝑌 = 𝑦 ) ) → 𝑋 = 𝑌 ) )
76 34 75 sylbid ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑥 ∈ { 𝑋 , 𝑌 } ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) → 𝑋 = 𝑌 ) )
77 76 adantld ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ { 𝑍 , 𝑍 } ∧ ∀ 𝑥 ∈ { 𝑋 , 𝑌 } ∀ 𝑦 ∈ { 𝑋 , 𝑌 } ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → 𝑋 = 𝑌 ) )
78 23 77 biimtrid ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐹 : { 𝑋 , 𝑌 } –1-1→ { 𝑍 , 𝑍 } → 𝑋 = 𝑌 ) )
79 22 78 biimtrrid ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐹 : { 𝑋 , 𝑌 } ⟶ { 𝑍 , 𝑍 } ∧ Fun ◡ 𝐹 ) → 𝑋 = 𝑌 ) )
80 21 79 mpand ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( Fun ◡ 𝐹 → 𝑋 = 𝑌 ) )
81 16 80 mtod ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ¬ Fun ◡ 𝐹 )
82 14 81 jca ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑋 ≠ 𝑌 ) → ( Fun 𝐹 ∧ ¬ Fun ◡ 𝐹 ) )