Theorem hashdmprop2dom 11011

Description: A class which contains two ordered pairs with different first components has at least two elements. (Contributed by AV, 12-Nov-2021.)

Hypotheses

Ref	Expression
hashdmpropge2.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
hashdmpropge2.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)
hashdmpropge2.c	⊢ (𝜑 → 𝐶 ∈ 𝑋)
hashdmpropge2.d	⊢ (𝜑 → 𝐷 ∈ 𝑌)
hashdmpropge2.f	⊢ (𝜑 → 𝐹 ∈ 𝑍)
hashdmpropge2.n	⊢ (𝜑 → 𝐴 ≠ 𝐵)
hashdmpropge2.s	⊢ (𝜑 → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} ⊆ 𝐹)

Assertion

Ref	Expression
hashdmprop2dom	⊢ (𝜑 → 2o ≼ dom 𝐹)

Proof of Theorem hashdmprop2dom

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hashdmpropge2.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝑍)
2	1	dmexd 4953	. 2 ⊢ (𝜑 → dom 𝐹 ∈ V)
3		hashdmpropge2.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
4		hashdmpropge2.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ 𝑌)
5		dmpropg 5164	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → dom {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = {𝐴, 𝐵})
6	3, 4, 5	syl2anc 411	. . . . . 6 ⊢ (𝜑 → dom {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = {𝐴, 𝐵})
7		hashdmpropge2.s	. . . . . . 7 ⊢ (𝜑 → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} ⊆ 𝐹)
8		dmss 4886	. . . . . . 7 ⊢ ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} ⊆ 𝐹 → dom {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} ⊆ dom 𝐹)
9	7, 8	syl 14	. . . . . 6 ⊢ (𝜑 → dom {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} ⊆ dom 𝐹)
10	6, 9	eqsstrrd 3234	. . . . 5 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ dom 𝐹)
11		hashdmpropge2.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
12		hashdmpropge2.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
13		prssg 3796	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ dom 𝐹) ↔ {𝐴, 𝐵} ⊆ dom 𝐹))
14	11, 12, 13	syl2anc 411	. . . . 5 ⊢ (𝜑 → ((𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ dom 𝐹) ↔ {𝐴, 𝐵} ⊆ dom 𝐹))
15	10, 14	mpbird 167	. . . 4 ⊢ (𝜑 → (𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ dom 𝐹))
16	15	simpld 112	. . 3 ⊢ (𝜑 → 𝐴 ∈ dom 𝐹)
17	15	simprd 114	. . 3 ⊢ (𝜑 → 𝐵 ∈ dom 𝐹)
18		hashdmpropge2.n	. . 3 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
19		neeq1 2390	. . . 4 ⊢ (𝑎 = 𝐴 → (𝑎 ≠ 𝑏 ↔ 𝐴 ≠ 𝑏))
20		neeq2 2391	. . . 4 ⊢ (𝑏 = 𝐵 → (𝐴 ≠ 𝑏 ↔ 𝐴 ≠ 𝐵))
21	19, 20	rspc2ev 2896	. . 3 ⊢ ((𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ dom 𝐹 ∧ 𝐴 ≠ 𝐵) → ∃𝑎 ∈ dom 𝐹∃𝑏 ∈ dom 𝐹 𝑎 ≠ 𝑏)
22	16, 17, 18, 21	syl3anc 1250	. 2 ⊢ (𝜑 → ∃𝑎 ∈ dom 𝐹∃𝑏 ∈ dom 𝐹 𝑎 ≠ 𝑏)
23		rex2dom 6924	. 2 ⊢ ((dom 𝐹 ∈ V ∧ ∃𝑎 ∈ dom 𝐹∃𝑏 ∈ dom 𝐹 𝑎 ≠ 𝑏) → 2o ≼ dom 𝐹)
24	2, 22, 23	syl2anc 411	1 ⊢ (𝜑 → 2o ≼ dom 𝐹)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1373   ∈ wcel 2177   ≠ wne 2377  ∃wrex 2486  Vcvv 2773   ⊆ wss 3170  {cpr 3639  ⟨cop 3641   class class class wbr 4051  dom cdm 4683  2_oc2o 6509   ≼ cdom 6839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-nul 4178  ax-pow 4226  ax-pr 4261  ax-un 4488

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-ral 2490  df-rex 2491  df-v 2775  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-nul 3465  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-opab 4114  df-tr 4151  df-id 4348  df-iord 4421  df-on 4423  df-suc 4426  df-xp 4689  df-rel 4690  df-cnv 4691  df-co 4692  df-dm 4693  df-rn 4694  df-fun 5282  df-fn 5283  df-f 5284  df-f1 5285  df-fo 5286  df-f1o 5287  df-1o 6515  df-2o 6516  df-en 6841  df-dom 6842

This theorem is referenced by:  struct2slots2dom  15712  structgr2slots2dom  15715