Theorem brdomi 9000

Description: Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.) Avoid ax-un 7761. (Revised by BTernaryTau, 29-Nov-2024.)

Assertion

Ref	Expression
brdomi	⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵)

Distinct variable groups:   𝐴,𝑓   𝐵,𝑓

Proof of Theorem brdomi

Step	Hyp	Ref	Expression
1		reldom 8993	. . . 4 ⊢ Rel ≼
2	1	brrelex12i 5710	. . 3 ⊢ (𝐴 ≼ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3		brdom2g 8998	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
4	2, 3	syl 18	. 2 ⊢ (𝐴 ≼ 𝐵 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
5	4	ibi 270	1 ⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1811   ∈ wcel 2146  Vcvv 3454   class class class wbr 5106  –1-1→wf1 6544   ≼ cdom 8985

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662  df-fn 6550  df-f 6551  df-f1 6552  df-dom 8989

This theorem is used by:  domssl  9039  domssr  9040  2dom  9072  undom  9098  xpdom2  9105  domunsncan  9110  dom0  9138  fodomr  9161  domssex  9171  domtrfil  9221  sucdom2  9232  sdom1  9255  1sdom2dom  9259  infn0  9308  fodomfir  9333  hartogslem1  9549  infdifsn  9671  acndom  10143  acndom2  10146  fictb  10335  fin23lem41  10443  iundom2g  10637  pwfseq  10762  omssubadd  34988