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 → A B ⊆ 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 ↔ A B = 2
5 4 biimpi ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → A B = 2
6 1 2 3 5 syl3an ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = 2
7 6 ad2antrr ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ C ∈ U ∧ A B ⊆ C → A B = 2
8 hashss ⊢ C ∈ U ∧ A B ⊆ C → A B ≤ C
9 8 adantll ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ C ∈ U ∧ A B ⊆ C → A B ≤ C
10 7 9 eqbrtrrd ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ C ∈ U ∧ A B ⊆ C → 2 ≤ C
11 10 ex ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ C ∈ U → A B ⊆ C → 2 ≤ C