Metamath Proof Explorer

Theorem prsshashgt1

Description: The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021)

Ref Expression
Assertion prsshashgt1 ⊢A∈V∧B∈W∧A≠B∧C∈U→AB⊆C→2≤C

Proof

Step Hyp Ref Expression
1 elex ⊢A∈V→A∈V
2 elex ⊢B∈W→B∈V
3 id ⊢A≠B→A≠B
4 hashprb ⊢A∈V∧B∈V∧A≠B↔AB=2
5 4 biimpi ⊢A∈V∧B∈V∧A≠B→AB=2
6 1 2 3 5 syl3an ⊢A∈V∧B∈W∧A≠B→AB=2
7 6 ad2antrr ⊢A∈V∧B∈W∧A≠B∧C∈U∧AB⊆C→AB=2
8 hashss ⊢C∈U∧AB⊆C→AB≤C
9 8 adantll ⊢A∈V∧B∈W∧A≠B∧C∈U∧AB⊆C→AB≤C
10 7 9 eqbrtrrd ⊢A∈V∧B∈W∧A≠B∧C∈U∧AB⊆C→2≤C
11 10 ex ⊢A∈V∧B∈W∧A≠B∧C∈U→AB⊆C→2≤C