Metamath Proof Explorer


Theorem hashdmpropge2

Description: The size of the domain of a class which contains two ordered pairs with different first components is greater than or equal to 2. (Contributed by AV, 12-Nov-2021)

Ref Expression
Hypotheses hashdmpropge2.a
|- ( ph -> A e. V )
hashdmpropge2.b
|- ( ph -> B e. W )
hashdmpropge2.c
|- ( ph -> C e. X )
hashdmpropge2.d
|- ( ph -> D e. Y )
hashdmpropge2.f
|- ( ph -> F e. Z )
hashdmpropge2.n
|- ( ph -> A =/= B )
hashdmpropge2.s
|- ( ph -> { <. A , C >. , <. B , D >. } C_ F )
Assertion hashdmpropge2
|- ( ph -> 2 <_ ( # ` dom F ) )

Proof

Step Hyp Ref Expression
1 hashdmpropge2.a
 |-  ( ph -> A e. V )
2 hashdmpropge2.b
 |-  ( ph -> B e. W )
3 hashdmpropge2.c
 |-  ( ph -> C e. X )
4 hashdmpropge2.d
 |-  ( ph -> D e. Y )
5 hashdmpropge2.f
 |-  ( ph -> F e. Z )
6 hashdmpropge2.n
 |-  ( ph -> A =/= B )
7 hashdmpropge2.s
 |-  ( ph -> { <. A , C >. , <. B , D >. } C_ F )
8 5 dmexd
 |-  ( ph -> dom F e. _V )
9 dmpropg
 |-  ( ( C e. X /\ D e. Y ) -> dom { <. A , C >. , <. B , D >. } = { A , B } )
10 3 4 9 syl2anc
 |-  ( ph -> dom { <. A , C >. , <. B , D >. } = { A , B } )
11 dmss
 |-  ( { <. A , C >. , <. B , D >. } C_ F -> dom { <. A , C >. , <. B , D >. } C_ dom F )
12 7 11 syl
 |-  ( ph -> dom { <. A , C >. , <. B , D >. } C_ dom F )
13 10 12 eqsstrrd
 |-  ( ph -> { A , B } C_ dom F )
14 prssg
 |-  ( ( A e. V /\ B e. W ) -> ( ( A e. dom F /\ B e. dom F ) <-> { A , B } C_ dom F ) )
15 1 2 14 syl2anc
 |-  ( ph -> ( ( A e. dom F /\ B e. dom F ) <-> { A , B } C_ dom F ) )
16 neeq1
 |-  ( a = A -> ( a =/= b <-> A =/= b ) )
17 neeq2
 |-  ( b = B -> ( A =/= b <-> A =/= B ) )
18 16 17 rspc2ev
 |-  ( ( A e. dom F /\ B e. dom F /\ A =/= B ) -> E. a e. dom F E. b e. dom F a =/= b )
19 18 3expa
 |-  ( ( ( A e. dom F /\ B e. dom F ) /\ A =/= B ) -> E. a e. dom F E. b e. dom F a =/= b )
20 19 expcom
 |-  ( A =/= B -> ( ( A e. dom F /\ B e. dom F ) -> E. a e. dom F E. b e. dom F a =/= b ) )
21 6 20 syl
 |-  ( ph -> ( ( A e. dom F /\ B e. dom F ) -> E. a e. dom F E. b e. dom F a =/= b ) )
22 15 21 sylbird
 |-  ( ph -> ( { A , B } C_ dom F -> E. a e. dom F E. b e. dom F a =/= b ) )
23 13 22 mpd
 |-  ( ph -> E. a e. dom F E. b e. dom F a =/= b )
24 hashge2el2difr
 |-  ( ( dom F e. _V /\ E. a e. dom F E. b e. dom F a =/= b ) -> 2 <_ ( # ` dom F ) )
25 8 23 24 syl2anc
 |-  ( ph -> 2 <_ ( # ` dom F ) )