Metamath Proof Explorer


Theorem abrexdom

Description: An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypothesis abrexdom.1 y A * x φ
Assertion abrexdom A V x | y A φ A

Proof

Step Hyp Ref Expression
1 abrexdom.1 y A * x φ
2 df-rex y A φ y y A φ
3 2 abbii x | y A φ = x | y y A φ
4 rnopab ran y x | y A φ = x | y y A φ
5 3 4 eqtr4i x | y A φ = ran y x | y A φ
6 dmopabss dom y x | y A φ A
7 ssexg dom y x | y A φ A A V dom y x | y A φ V
8 6 7 mpan A V dom y x | y A φ V
9 funopab Fun y x | y A φ y * x y A φ
10 moanimv * x y A φ y A * x φ
11 1 10 mpbir * x y A φ
12 9 11 mpgbir Fun y x | y A φ
13 12 a1i A V Fun y x | y A φ
14 funfn Fun y x | y A φ y x | y A φ Fn dom y x | y A φ
15 13 14 sylib A V y x | y A φ Fn dom y x | y A φ
16 fnrndomg dom y x | y A φ V y x | y A φ Fn dom y x | y A φ ran y x | y A φ dom y x | y A φ
17 8 15 16 sylc A V ran y x | y A φ dom y x | y A φ
18 ssdomg A V dom y x | y A φ A dom y x | y A φ A
19 6 18 mpi A V dom y x | y A φ A
20 domtr ran y x | y A φ dom y x | y A φ dom y x | y A φ A ran y x | y A φ A
21 17 19 20 syl2anc A V ran y x | y A φ A
22 5 21 eqbrtrid A V x | y A φ A