Theorem iundom

Description: An upper bound for the cardinality of an indexed union. C depends on x and should be thought of as C ( x ) . (Contributed by NM, 26-Mar-2006)

	Ref	Expression
Assertion	iundom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝐶 ≼ ( 𝐴 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 )
2		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → 𝐴 ∈ 𝑉 )
3		ovex	⊢ ( 𝐵 ↑m 𝐶 ) ∈ V
4	3	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ V
5		iunexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ V ) → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ V )
6	2 4 5	sylancl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ V )
7		numth3	⊢ ( ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ V → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ dom card )
8	6 7	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ dom card )
9		numacn	⊢ ( 𝐴 ∈ 𝑉 → ( ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ dom card → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ AC 𝐴 ) )
10	2 8 9	sylc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ AC 𝐴 )
11		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 )
12		reldom	⊢ Rel ≼
13	12	brrelex1i	⊢ ( 𝐶 ≼ 𝐵 → 𝐶 ∈ V )
14	13	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V )
15		iunexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V ) → ∪ 𝑥 ∈ 𝐴 𝐶 ∈ V )
16	14 15	sylan2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝐶 ∈ V )
17	1 10 11	iundom2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) ≼ ( 𝐴 × 𝐵 ) )
18	12	brrelex2i	⊢ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) ≼ ( 𝐴 × 𝐵 ) → ( 𝐴 × 𝐵 ) ∈ V )
19		numth3	⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ( 𝐴 × 𝐵 ) ∈ dom card )
20	17 18 19	3syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ( 𝐴 × 𝐵 ) ∈ dom card )
21		numacn	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐶 ∈ V → ( ( 𝐴 × 𝐵 ) ∈ dom card → ( 𝐴 × 𝐵 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐶 ) )
22	16 20 21	sylc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ( 𝐴 × 𝐵 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐶 )
23	1 10 11 22	iundomg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝐶 ≼ ( 𝐴 × 𝐵 ) )