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	$⊢ φ \to A \in V$
	hashdmpropge2.b	$⊢ φ \to B \in W$
	hashdmpropge2.c	$⊢ φ \to C \in X$
	hashdmpropge2.d	$⊢ φ \to D \in Y$
	hashdmpropge2.f	$⊢ φ \to F \in Z$
	hashdmpropge2.n	$⊢ φ \to A \neq B$
	hashdmpropge2.s	$⊢ φ \to \{⟨A, C⟩, ⟨B, D⟩\} \subseteq F$
Assertion	hashdmpropge2	$⊢ φ \to 2 \leq \|dom F\|$

Proof

Step	Hyp	Ref	Expression
1		hashdmpropge2.a	$⊢ φ \to A \in V$
2		hashdmpropge2.b	$⊢ φ \to B \in W$
3		hashdmpropge2.c	$⊢ φ \to C \in X$
4		hashdmpropge2.d	$⊢ φ \to D \in Y$
5		hashdmpropge2.f	$⊢ φ \to F \in Z$
6		hashdmpropge2.n	$⊢ φ \to A \neq B$
7		hashdmpropge2.s	$⊢ φ \to \{⟨A, C⟩, ⟨B, D⟩\} \subseteq F$
8	5	dmexd	$⊢ φ \to dom F \in V$
9		dmpropg	$⊢ (C \in X \land D \in Y) \to dom \{⟨A, C⟩, ⟨B, D⟩\} = \{A, B\}$
10	3 4 9	syl2anc	$⊢ φ \to dom \{⟨A, C⟩, ⟨B, D⟩\} = \{A, B\}$
11		dmss	$⊢ \{⟨A, C⟩, ⟨B, D⟩\} \subseteq F \to dom \{⟨A, C⟩, ⟨B, D⟩\} \subseteq dom F$
12	7 11	syl	$⊢ φ \to dom \{⟨A, C⟩, ⟨B, D⟩\} \subseteq dom F$
13	10 12	eqsstrrd	$⊢ φ \to \{A, B\} \subseteq dom F$
14		prssg	$⊢ (A \in V \land B \in W) \to ((A \in dom F \land B \in dom F) \leftrightarrow \{A, B\} \subseteq dom F)$
15	1 2 14	syl2anc	$⊢ φ \to ((A \in dom F \land B \in dom F) \leftrightarrow \{A, B\} \subseteq dom F)$
16		neeq1	$⊢ a = A \to (a \neq b \leftrightarrow A \neq b)$
17		neeq2	$⊢ b = B \to (A \neq b \leftrightarrow A \neq B)$
18	16 17	rspc2ev	$⊢ (A \in dom F \land B \in dom F \land A \neq B) \to \exists a \in dom F \exists b \in dom F a \neq b$
19	18	3expa	$⊢ ((A \in dom F \land B \in dom F) \land A \neq B) \to \exists a \in dom F \exists b \in dom F a \neq b$
20	19	expcom	$⊢ A \neq B \to ((A \in dom F \land B \in dom F) \to \exists a \in dom F \exists b \in dom F a \neq b)$
21	6 20	syl	$⊢ φ \to ((A \in dom F \land B \in dom F) \to \exists a \in dom F \exists b \in dom F a \neq b)$
22	15 21	sylbird	$⊢ φ \to (\{A, B\} \subseteq dom F \to \exists a \in dom F \exists b \in dom F a \neq b)$
23	13 22	mpd	$⊢ φ \to \exists a \in dom F \exists b \in dom F a \neq b$
24		hashge2el2difr	$⊢ (dom F \in V \land \exists a \in dom F \exists b \in dom F a \neq b) \to 2 \leq \|dom F\|$
25	8 23 24	syl2anc	$⊢ φ \to 2 \leq \|dom F\|$

Metamath Proof Explorer

Theorem hashdmpropge2

Proof