Theorem iundomg

Description: An upper bound for the cardinality of an indexed union, with explicit choice principles. B depends on x and should be thought of as B ( x ) . (Contributed by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Hypotheses	iunfo.1	⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
	iundomg.2	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↑m 𝐵 ) ∈ AC 𝐴 )
	iundomg.3	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≼ 𝐶 )
	iundomg.4	⊢ ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 )
Assertion	iundomg	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ( 𝐴 × 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		iunfo.1	⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
2		iundomg.2	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↑m 𝐵 ) ∈ AC 𝐴 )
3		iundomg.3	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≼ 𝐶 )
4		iundomg.4	⊢ ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 )
5	1 2 3	iundom2g	⊢ ( 𝜑 → 𝑇 ≼ ( 𝐴 × 𝐶 ) )
6		acndom2	⊢ ( 𝑇 ≼ ( 𝐴 × 𝐶 ) → ( ( 𝐴 × 𝐶 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑇 ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 ) )
7	5 4 6	sylc	⊢ ( 𝜑 → 𝑇 ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 )
8	1	iunfo	⊢ ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵
9		fodomacn	⊢ ( 𝑇 ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 → ( ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ 𝑇 ) )
10	7 8 9	mpisyl	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ 𝑇 )
11		domtr	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ≼ 𝑇 ∧ 𝑇 ≼ ( 𝐴 × 𝐶 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ( 𝐴 × 𝐶 ) )
12	10 5 11	syl2anc	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ( 𝐴 × 𝐶 ) )