Theorem brdomi 8748

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∃wex 1782   ∈ wcel 2106  Vcvv 3432   class class class wbr 5074  –1-1→wf1 6430   ≼ cdom 8731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-fn 6436  df-f 6437  df-f1 6438  df-dom 8735

This theorem is referenced by:  2dom  8820  undom  8846  xpdom2  8854  domunsncan  8859  sucdom2OLD  8869  dom0  8889  fodomr  8915  domssex  8925  domtrfil  8978  sucdom2  8989  hartogslem1  9301  infdifsn  9415  acndom  9807  acndom2  9810  fictb  10001  fin23lem41  10108  iundom2g  10296  pwfseq  10420  omssubadd  32267