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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	hashdmpropge2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	hashdmpropge2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	hashdmpropge2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
	hashdmpropge2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑍 )
	hashdmpropge2.n	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	hashdmpropge2.s	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ⊆ 𝐹 )
Assertion	hashdmpropge2	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		hashdmpropge2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		hashdmpropge2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		hashdmpropge2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
4		hashdmpropge2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
5		hashdmpropge2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑍 )
6		hashdmpropge2.n	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
7		hashdmpropge2.s	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ⊆ 𝐹 )
8	5	dmexd	⊢ ( 𝜑 → dom 𝐹 ∈ V )
9		dmpropg	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) → dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐴 , 𝐵 } )
10	3 4 9	syl2anc	⊢ ( 𝜑 → dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐴 , 𝐵 } )
11		dmss	⊢ ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ⊆ 𝐹 → dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ⊆ dom 𝐹 )
12	7 11	syl	⊢ ( 𝜑 → dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ⊆ dom 𝐹 )
13	10 12	eqsstrrd	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ dom 𝐹 )
14		prssg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) ↔ { 𝐴 , 𝐵 } ⊆ dom 𝐹 ) )
15	1 2 14	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) ↔ { 𝐴 , 𝐵 } ⊆ dom 𝐹 ) )
16		neeq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ≠ 𝑏 ↔ 𝐴 ≠ 𝑏 ) )
17		neeq2	⊢ ( 𝑏 = 𝐵 → ( 𝐴 ≠ 𝑏 ↔ 𝐴 ≠ 𝐵 ) )
18	16 17	rspc2ev	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ dom 𝐹 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 𝑎 ≠ 𝑏 )
19	18	3expa	⊢ ( ( ( 𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 𝑎 ≠ 𝑏 )
20	19	expcom	⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 𝑎 ≠ 𝑏 ) )
21	6 20	syl	⊢ ( 𝜑 → ( ( 𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 𝑎 ≠ 𝑏 ) )
22	15 21	sylbird	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ dom 𝐹 → ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 𝑎 ≠ 𝑏 ) )
23	13 22	mpd	⊢ ( 𝜑 → ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 𝑎 ≠ 𝑏 )
24		hashge2el2difr	⊢ ( ( dom 𝐹 ∈ V ∧ ∃ 𝑎 ∈ dom 𝐹 ∃ 𝑏 ∈ dom 𝐹 𝑎 ≠ 𝑏 ) → 2 ≤ ( ♯ ‘ dom 𝐹 ) )
25	8 23 24	syl2anc	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐹 ) )

Metamath Proof Explorer

Theorem hashdmpropge2

Proof