Theorem brdomi 8941

Description: Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.) Avoid ax-un 7719. (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 8934	. . . 4 ⊢ Rel ≼
2	1	brrelex12i 5703	. . 3 ⊢ (𝐴 ≼ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3		brdom2g 8939	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
4	2, 3	syl 17	. 2 ⊢ (𝐴 ≼ 𝐵 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
5	4	ibi 269	1 ⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∃wex 1800   ∈ wcel 2143  Vcvv 3455   class class class wbr 5101  –1-1→wf1 6519   ≼ cdom 8926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5247  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5102  df-opab 5164  df-xp 5654  df-rel 5655  df-fn 6525  df-f 6526  df-f1 6527  df-dom 8930

This theorem is referenced by:  domssl  8980  domssr  8981  2dom  9012  undom  9038  xpdom2  9045  domunsncan  9050  dom0  9078  fodomr  9101  domssex  9111  domtrfil  9161  sucdom2  9172  sdom1  9195  1sdom2dom  9199  infn0  9247  fodomfir  9273  hartogslem1  9491  infdifsn  9613  acndom  10008  acndom2  10011  fictb  10201  fin23lem41  10310  iundom2g  10498  pwfseq  10623  omssubadd  34598