Metamath Proof Explorer

Theorem fundmge2nop0

Description: A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fundmge2nop (with the less restrictive requirement that ( G \ { (/) } ) needs to be a function instead of G ) is useful for proofs for extensible structures, see structn0fun . (Contributed by AV, 12-Oct-2020) (Revised by AV, 7-Jun-2021) (Proof shortened by AV, 15-Nov-2021)

Ref Expression
Assertion fundmge2nop0 ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ¬ 𝐺 ∈ ( V × V ) )

Proof

Step Hyp Ref Expression
1 dmexg ⊢ ( 𝐺 ∈ V → dom 𝐺 ∈ V )
2 hashge2el2dif ⊢ ( ( dom 𝐺 ∈ V ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ∃ 𝑎 ∈ dom 𝐺 ∃ 𝑏 ∈ dom 𝐺 𝑎 ≠ 𝑏 )
3 2 ex ⊢ ( dom 𝐺 ∈ V → ( 2 ≤ ( ♯ ‘ dom 𝐺 ) → ∃ 𝑎 ∈ dom 𝐺 ∃ 𝑏 ∈ dom 𝐺 𝑎 ≠ 𝑏 ) )
4 1 3 syl ⊢ ( 𝐺 ∈ V → ( 2 ≤ ( ♯ ‘ dom 𝐺 ) → ∃ 𝑎 ∈ dom 𝐺 ∃ 𝑏 ∈ dom 𝐺 𝑎 ≠ 𝑏 ) )
5 df-ne ⊢ ( 𝑎 ≠ 𝑏 ↔ ¬ 𝑎 = 𝑏 )
6 elvv ⊢ ( 𝐺 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ )
7 difeq1 ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺 ∖ { ∅ } ) = ( ⟨ 𝑥 , 𝑦 ⟩ ∖ { ∅ } ) )
8 7 funeqd ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( Fun ( 𝐺 ∖ { ∅ } ) ↔ Fun ( ⟨ 𝑥 , 𝑦 ⟩ ∖ { ∅ } ) ) )
9 opwo0id ⊢ ⟨ 𝑥 , 𝑦 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ ∖ { ∅ } )
10 9 eqcomi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∖ { ∅ } ) = ⟨ 𝑥 , 𝑦 ⟩
11 10 funeqi ⊢ ( Fun ( ⟨ 𝑥 , 𝑦 ⟩ ∖ { ∅ } ) ↔ Fun ⟨ 𝑥 , 𝑦 ⟩ )
12 dmeq ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → dom 𝐺 = dom ⟨ 𝑥 , 𝑦 ⟩ )
13 12 eleq2d ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑎 ∈ dom 𝐺 ↔ 𝑎 ∈ dom ⟨ 𝑥 , 𝑦 ⟩ ) )
14 12 eleq2d ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑏 ∈ dom 𝐺 ↔ 𝑏 ∈ dom ⟨ 𝑥 , 𝑦 ⟩ ) )
15 13 14 anbi12d ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) ↔ ( 𝑎 ∈ dom ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑏 ∈ dom ⟨ 𝑥 , 𝑦 ⟩ ) ) )
16 eqid ⊢ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
17 vex ⊢ 𝑥 ∈ V
18 vex ⊢ 𝑦 ∈ V
19 16 17 18 funopdmsn ⊢ ( ( Fun ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑎 ∈ dom ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑏 ∈ dom ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑎 = 𝑏 )
20 19 3expb ⊢ ( ( Fun ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑎 ∈ dom ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑏 ∈ dom ⟨ 𝑥 , 𝑦 ⟩ ) ) → 𝑎 = 𝑏 )
21 20 expcom ⊢ ( ( 𝑎 ∈ dom ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑏 ∈ dom ⟨ 𝑥 , 𝑦 ⟩ ) → ( Fun ⟨ 𝑥 , 𝑦 ⟩ → 𝑎 = 𝑏 ) )
22 15 21 syl6bi ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) → ( Fun ⟨ 𝑥 , 𝑦 ⟩ → 𝑎 = 𝑏 ) ) )
23 22 com23 ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( Fun ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) → 𝑎 = 𝑏 ) ) )
24 11 23 syl5bi ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( Fun ( ⟨ 𝑥 , 𝑦 ⟩ ∖ { ∅ } ) → ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) → 𝑎 = 𝑏 ) ) )
25 8 24 sylbid ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( Fun ( 𝐺 ∖ { ∅ } ) → ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) → 𝑎 = 𝑏 ) ) )
26 25 impcomd ⊢ ( 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → 𝑎 = 𝑏 ) )
27 26 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → 𝑎 = 𝑏 ) )
28 27 com12 ⊢ ( ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → ( ∃ 𝑥 ∃ 𝑦 𝐺 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑎 = 𝑏 ) )
29 6 28 syl5bi ⊢ ( ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → ( 𝐺 ∈ ( V × V ) → 𝑎 = 𝑏 ) )
30 29 con3d ⊢ ( ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → ( ¬ 𝑎 = 𝑏 → ¬ 𝐺 ∈ ( V × V ) ) )
31 30 ex ⊢ ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) → ( Fun ( 𝐺 ∖ { ∅ } ) → ( ¬ 𝑎 = 𝑏 → ¬ 𝐺 ∈ ( V × V ) ) ) )
32 31 com23 ⊢ ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) → ( ¬ 𝑎 = 𝑏 → ( Fun ( 𝐺 ∖ { ∅ } ) → ¬ 𝐺 ∈ ( V × V ) ) ) )
33 5 32 syl5bi ⊢ ( ( 𝑎 ∈ dom 𝐺 ∧ 𝑏 ∈ dom 𝐺 ) → ( 𝑎 ≠ 𝑏 → ( Fun ( 𝐺 ∖ { ∅ } ) → ¬ 𝐺 ∈ ( V × V ) ) ) )
34 33 rexlimivv ⊢ ( ∃ 𝑎 ∈ dom 𝐺 ∃ 𝑏 ∈ dom 𝐺 𝑎 ≠ 𝑏 → ( Fun ( 𝐺 ∖ { ∅ } ) → ¬ 𝐺 ∈ ( V × V ) ) )
35 4 34 syl6 ⊢ ( 𝐺 ∈ V → ( 2 ≤ ( ♯ ‘ dom 𝐺 ) → ( Fun ( 𝐺 ∖ { ∅ } ) → ¬ 𝐺 ∈ ( V × V ) ) ) )
36 35 com13 ⊢ ( Fun ( 𝐺 ∖ { ∅ } ) → ( 2 ≤ ( ♯ ‘ dom 𝐺 ) → ( 𝐺 ∈ V → ¬ 𝐺 ∈ ( V × V ) ) ) )
37 36 imp ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ( 𝐺 ∈ V → ¬ 𝐺 ∈ ( V × V ) ) )
38 prcnel ⊢ ( ¬ 𝐺 ∈ V → ¬ 𝐺 ∈ ( V × V ) )
39 37 38 pm2.61d1 ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ¬ 𝐺 ∈ ( V × V ) )