Metamath Proof Explorer

Theorem wdomima2g

Description: A set is weakly dominant over its image under any function. This version of wdomimag is stated so as to avoid ax-rep . (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion wdomima2g ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → ( 𝐹 “ 𝐴 ) ≼* 𝐴 )

Proof

Step Hyp Ref Expression
1 df-ima ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
2 funres ⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐴 ) )
3 funforn ⊢ ( Fun ( 𝐹 ↾ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) )
4 2 3 sylib ⊢ ( Fun 𝐹 → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) )
5 4 3ad2ant1 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) )
6 fof ⊢ ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ran ( 𝐹 ↾ 𝐴 ) )
7 5 6 syl ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ran ( 𝐹 ↾ 𝐴 ) )
8 dmres ⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
9 inss1 ⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴
10 8 9 eqsstri ⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴
11 simp2 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → 𝐴 ∈ 𝑉 )
12 ssexg ⊢ ( ( dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → dom ( 𝐹 ↾ 𝐴 ) ∈ V )
13 10 11 12 sylancr ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → dom ( 𝐹 ↾ 𝐴 ) ∈ V )
14 simp3 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → ( 𝐹 “ 𝐴 ) ∈ 𝑊 )
15 1 14 eqeltrrid ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → ran ( 𝐹 ↾ 𝐴 ) ∈ 𝑊 )
16 fex2 ⊢ ( ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ran ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) ∈ V ∧ ran ( 𝐹 ↾ 𝐴 ) ∈ 𝑊 ) → ( 𝐹 ↾ 𝐴 ) ∈ V )
17 7 13 15 16 syl3anc ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → ( 𝐹 ↾ 𝐴 ) ∈ V )
18 fowdom ⊢ ( ( ( 𝐹 ↾ 𝐴 ) ∈ V ∧ ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) ) → ran ( 𝐹 ↾ 𝐴 ) ≼* dom ( 𝐹 ↾ 𝐴 ) )
19 17 5 18 syl2anc ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → ran ( 𝐹 ↾ 𝐴 ) ≼* dom ( 𝐹 ↾ 𝐴 ) )
20 ssdomg ⊢ ( 𝐴 ∈ 𝑉 → ( dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 → dom ( 𝐹 ↾ 𝐴 ) ≼ 𝐴 ) )
21 10 20 mpi ⊢ ( 𝐴 ∈ 𝑉 → dom ( 𝐹 ↾ 𝐴 ) ≼ 𝐴 )
22 domwdom ⊢ ( dom ( 𝐹 ↾ 𝐴 ) ≼ 𝐴 → dom ( 𝐹 ↾ 𝐴 ) ≼* 𝐴 )
23 21 22 syl ⊢ ( 𝐴 ∈ 𝑉 → dom ( 𝐹 ↾ 𝐴 ) ≼* 𝐴 )
24 23 3ad2ant2 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → dom ( 𝐹 ↾ 𝐴 ) ≼* 𝐴 )
25 wdomtr ⊢ ( ( ran ( 𝐹 ↾ 𝐴 ) ≼* dom ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) ≼* 𝐴 ) → ran ( 𝐹 ↾ 𝐴 ) ≼* 𝐴 )
26 19 24 25 syl2anc ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → ran ( 𝐹 ↾ 𝐴 ) ≼* 𝐴 )
27 1 26 eqbrtrid ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐹 “ 𝐴 ) ∈ 𝑊 ) → ( 𝐹 “ 𝐴 ) ≼* 𝐴 )