Metamath Proof Explorer


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 ( 𝜑 𝑥𝐴 𝐵 ≼ ( 𝐴 × 𝐶 ) )