Theorem abrexdomjm

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

	Ref	Expression
Hypothesis	abrexdomjm.1	⊢ ( 𝑦 ∈ 𝐴 → ∃* 𝑥 𝜑 )
Assertion	abrexdomjm	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝜑 } ≼ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		abrexdomjm.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	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝜑 } ≼ 𝐴 )