Theorem imaexALTV

Description: Existence of an image of a class. Theorem 3.17 of Monk1 p. 39. (cf. imaexg ) with weakened antecedent: only the restricion of A by a set needs to be a set, not A itself, see e.g. cnvepimaex . (Contributed by Peter Mazsa, 22-Feb-2023) (Proof modification is discouraged.)

	Ref	Expression
Assertion	imaexALTV	⊢ ( ( 𝐴 ∈ 𝑉 ∨ ( ( 𝐴 ↾ 𝐵 ) ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 “ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		imassrn	⊢ ( 𝐴 “ 𝐵 ) ⊆ ran 𝐴
2		rnexg	⊢ ( 𝐴 ∈ 𝑉 → ran 𝐴 ∈ V )
3		ssexg	⊢ ( ( ( 𝐴 “ 𝐵 ) ⊆ ran 𝐴 ∧ ran 𝐴 ∈ V ) → ( 𝐴 “ 𝐵 ) ∈ V )
4	1 2 3	sylancr	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 “ 𝐵 ) ∈ V )
5		qsexg	⊢ ( 𝐵 ∈ 𝑋 → ( 𝐵 / 𝐴 ) ∈ V )
6		uniexg	⊢ ( ( 𝐵 / 𝐴 ) ∈ V → ∪ ( 𝐵 / 𝐴 ) ∈ V )
7	5 6	syl	⊢ ( 𝐵 ∈ 𝑋 → ∪ ( 𝐵 / 𝐴 ) ∈ V )
8		uniqsALTV	⊢ ( ( 𝐴 ↾ 𝐵 ) ∈ 𝑊 → ∪ ( 𝐵 / 𝐴 ) = ( 𝐴 “ 𝐵 ) )
9	8	eleq1d	⊢ ( ( 𝐴 ↾ 𝐵 ) ∈ 𝑊 → ( ∪ ( 𝐵 / 𝐴 ) ∈ V ↔ ( 𝐴 “ 𝐵 ) ∈ V ) )
10	7 9	syl5ib	⊢ ( ( 𝐴 ↾ 𝐵 ) ∈ 𝑊 → ( 𝐵 ∈ 𝑋 → ( 𝐴 “ 𝐵 ) ∈ V ) )
11	10	imp	⊢ ( ( ( 𝐴 ↾ 𝐵 ) ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 “ 𝐵 ) ∈ V )
12	4 11	jaoi	⊢ ( ( 𝐴 ∈ 𝑉 ∨ ( ( 𝐴 ↾ 𝐵 ) ∈ 𝑊 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 “ 𝐵 ) ∈ V )