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 ( 𝑦𝐴 → ∃* 𝑥 𝜑 )
Assertion abrexdom ( 𝐴𝑉 → { 𝑥 ∣ ∃ 𝑦𝐴 𝜑 } ≼ 𝐴 )

Proof

Step Hyp Ref Expression
1 abrexdom.1 ( 𝑦𝐴 → ∃* 𝑥 𝜑 )
2 df-rex ( ∃ 𝑦𝐴 𝜑 ↔ ∃ 𝑦 ( 𝑦𝐴𝜑 ) )
3 2 abbii { 𝑥 ∣ ∃ 𝑦𝐴 𝜑 } = { 𝑥 ∣ ∃ 𝑦 ( 𝑦𝐴𝜑 ) }
4 rnopab ran { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑦𝐴𝜑 ) }
5 3 4 eqtr4i { 𝑥 ∣ ∃ 𝑦𝐴 𝜑 } = ran { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) }
6 dmopabss dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ⊆ 𝐴
7 ssexg ( ( dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ⊆ 𝐴𝐴𝑉 ) → dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ∈ V )
8 6 7 mpan ( 𝐴𝑉 → dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ∈ V )
9 funopab ( Fun { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑦𝐴𝜑 ) )
10 moanimv ( ∃* 𝑥 ( 𝑦𝐴𝜑 ) ↔ ( 𝑦𝐴 → ∃* 𝑥 𝜑 ) )
11 1 10 mpbir ∃* 𝑥 ( 𝑦𝐴𝜑 )
12 9 11 mpgbir Fun { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) }
13 12 a1i ( 𝐴𝑉 → Fun { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } )
14 funfn ( Fun { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ↔ { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } Fn dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } )
15 13 14 sylib ( 𝐴𝑉 → { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } Fn dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } )
16 fnrndomg ( dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ∈ V → ( { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } Fn dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } → ran { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ≼ dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ) )
17 8 15 16 sylc ( 𝐴𝑉 → ran { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ≼ dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } )
18 ssdomg ( 𝐴𝑉 → ( dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ⊆ 𝐴 → dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ≼ 𝐴 ) )
19 6 18 mpi ( 𝐴𝑉 → dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ≼ 𝐴 )
20 domtr ( ( ran { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ≼ dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ∧ dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ≼ 𝐴 ) → ran { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ≼ 𝐴 )
21 17 19 20 syl2anc ( 𝐴𝑉 → ran { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦𝐴𝜑 ) } ≼ 𝐴 )
22 5 21 eqbrtrid ( 𝐴𝑉 → { 𝑥 ∣ ∃ 𝑦𝐴 𝜑 } ≼ 𝐴 )