Metamath Proof Explorer

Theorem fun2dmnop0

Description: A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop (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, 21-Sep-2020) (Revised by AV, 7-Jun-2021)

Ref Expression
Hypotheses fun2dmnop.a ⊢ 𝐴 ∈ V
fun2dmnop.b ⊢ 𝐵 ∈ V
Assertion fun2dmnop0 ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) → ¬ 𝐺 ∈ ( V × V ) )

Proof

Step Hyp Ref Expression
1 fun2dmnop.a ⊢ 𝐴 ∈ V
2 fun2dmnop.b ⊢ 𝐵 ∈ V
3 simpl1 ⊢ ( ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) ∧ 𝐺 ∈ V ) → Fun ( 𝐺 ∖ { ∅ } ) )
4 dmexg ⊢ ( 𝐺 ∈ V → dom 𝐺 ∈ V )
5 4 adantl ⊢ ( ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) ∧ 𝐺 ∈ V ) → dom 𝐺 ∈ V )
6 1 2 prss ⊢ ( ( 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) ↔ { 𝐴 , 𝐵 } ⊆ dom 𝐺 )
7 simpl ⊢ ( ( 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) → 𝐴 ∈ dom 𝐺 )
8 6 7 sylbir ⊢ ( { 𝐴 , 𝐵 } ⊆ dom 𝐺 → 𝐴 ∈ dom 𝐺 )
9 8 3ad2ant3 ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) → 𝐴 ∈ dom 𝐺 )
10 9 adantr ⊢ ( ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) ∧ 𝐺 ∈ V ) → 𝐴 ∈ dom 𝐺 )
11 simpr ⊢ ( ( 𝐴 ∈ dom 𝐺 ∧ 𝐵 ∈ dom 𝐺 ) → 𝐵 ∈ dom 𝐺 )
12 6 11 sylbir ⊢ ( { 𝐴 , 𝐵 } ⊆ dom 𝐺 → 𝐵 ∈ dom 𝐺 )
13 12 3ad2ant3 ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) → 𝐵 ∈ dom 𝐺 )
14 13 adantr ⊢ ( ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) ∧ 𝐺 ∈ V ) → 𝐵 ∈ dom 𝐺 )
15 simpl2 ⊢ ( ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) ∧ 𝐺 ∈ V ) → 𝐴 ≠ 𝐵 )
16 5 10 14 15 nehash2 ⊢ ( ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) ∧ 𝐺 ∈ V ) → 2 ≤ ( ♯ ‘ dom 𝐺 ) )
17 fundmge2nop0 ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ¬ 𝐺 ∈ ( V × V ) )
18 3 16 17 syl2anc ⊢ ( ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) ∧ 𝐺 ∈ V ) → ¬ 𝐺 ∈ ( V × V ) )
19 18 ex ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) → ( 𝐺 ∈ V → ¬ 𝐺 ∈ ( V × V ) ) )
20 prcnel ⊢ ( ¬ 𝐺 ∈ V → ¬ 𝐺 ∈ ( V × V ) )
21 19 20 pm2.61d1 ⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 𝐴 ≠ 𝐵 ∧ { 𝐴 , 𝐵 } ⊆ dom 𝐺 ) → ¬ 𝐺 ∈ ( V × V ) )