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 9614

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 3482	. 2 ⊢ (𝐹 ∈ 𝑉 → 𝐹 ∈ V)
2		foeq1 6811	. . . . . 6 ⊢ (𝑧 = 𝐹 → (𝑧:𝑌–onto→𝑋 ↔ 𝐹:𝑌–onto→𝑋))
3	2	spcegv 3583	. . . . 5 ⊢ (𝐹 ∈ V → (𝐹:𝑌–onto→𝑋 → ∃𝑧 𝑧:𝑌–onto→𝑋))
4	3	imp 405	. . . 4 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌–onto→𝑋) → ∃𝑧 𝑧:𝑌–onto→𝑋)
5	4	olcd 872	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌–onto→𝑋) → (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))
6		fof 6815	. . . . 5 ⊢ (𝐹:𝑌–onto→𝑋 → 𝐹:𝑌⟶𝑋)
7		dmfex 7918	. . . . 5 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌⟶𝑋) → 𝑌 ∈ V)
8	6, 7	sylan2 591	. . . 4 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌–onto→𝑋) → 𝑌 ∈ V)
9		brwdom 9610	. . . 4 ⊢ (𝑌 ∈ V → (𝑋 ≼^* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)))
10	8, 9	syl 17	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌–onto→𝑋) → (𝑋 ≼^* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)))
11	5, 10	mpbird 256	. 2 ⊢ ((𝐹 ∈ V ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼^* 𝑌)
12	1, 11	sylan 578	1 ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼^* 𝑌)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 845 = wceq 1534 ∃wex 1774 ∈ wcel 2099 Vcvv 3462 ∅c0 4325 class class class wbr 5153 ⟶wf 6550 –onto→wfo 6552 ≼^* cwdom 9607

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 ax-un 7746

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-opab 5216 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-fun 6556 df-fn 6557 df-f 6558 df-fo 6560 df-wdom 9608

This theorem is referenced by: wdomref 9615 wdomtr 9618 wdom2d 9623 wdomima2g 9629 ixpiunwdom 9633 harwdom 9634 isf32lem10 10405 fin1a2lem7 10449

W3C validator