fowdom - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fowdom		Structured version Visualization version GIF version

Theorem fowdom 9532

Description: An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.)

**Assertion**
Ref	Expression
fowdom	⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼^* 𝑌)

Proof of Theorem fowdom Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3484	. 2 ⊢ (𝐹 ∈ 𝑉 → 𝐹 ∈ V)
2		foeq1 6789	. . . . . 6 ⊢ (𝑧 = 𝐹 → (𝑧:𝑌–onto→𝑋 ↔ 𝐹:𝑌–onto→𝑋))
3	2	spcegv 3565	. . . . 5 ⊢ (𝐹 ∈ V → (𝐹:𝑌–onto→𝑋 → ∃𝑧 𝑧:𝑌–onto→𝑋))
4	3	imp 411	. . . 4 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌–onto→𝑋) → ∃𝑧 𝑧:𝑌–onto→𝑋)
5	4	olcd 887	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌–onto→𝑋) → (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))
6		fof 6793	. . . . 5 ⊢ (𝐹:𝑌–onto→𝑋 → 𝐹:𝑌⟶𝑋)
7		dmfex 7901	. . . . 5 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌⟶𝑋) → 𝑌 ∈ V)
8	6, 7	sylan2 604	. . . 4 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌–onto→𝑋) → 𝑌 ∈ V)
9		brwdom 9528	. . . 4 ⊢ (𝑌 ∈ V → (𝑋 ≼^* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)))
10	8, 9	syl 18	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌–onto→𝑋) → (𝑋 ≼^* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)))
11	5, 10	mpbird 260	. 2 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼^* 𝑌)
12	1, 11	sylan 591	1 ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼^* 𝑌)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1567 ∃wex 1806 ∈ wcel 2149 Vcvv 3463 ∅c0 4294 class class class wbr 5113 ⟶wf 6533 –onto→wfo 6535 ≼^* cwdom 9525

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-sb 2098 df-clab 2748 df-cleq 2761 df-clel 2844 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-fun 6539 df-fn 6540 df-f 6541 df-fo 6543 df-wdom 9526

This theorem is referenced by: wdomref 9533 wdomtr 9536 wdom2d 9541 wdomima2g 9547 ixpiunwdom 9551 harwdom 9552 isf32lem10 10345 fin1a2lem7 10389

W3C validator