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

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 ) )