Metamath Proof Explorer


Theorem uniimadom

Description: An upper bound for the cardinality of the union of an image. Theorem 10.48 of TakeutiZaring p. 99. (Contributed by NM, 25-Mar-2006)

Ref Expression
Hypotheses uniimadom.1 𝐴 ∈ V
uniimadom.2 𝐵 ∈ V
Assertion uniimadom ( ( Fun 𝐹 ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵 ) → ( 𝐹𝐴 ) ≼ ( 𝐴 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 uniimadom.1 𝐴 ∈ V
2 uniimadom.2 𝐵 ∈ V
3 1 funimaex ( Fun 𝐹 → ( 𝐹𝐴 ) ∈ V )
4 3 adantr ( ( Fun 𝐹 ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵 ) → ( 𝐹𝐴 ) ∈ V )
5 fvelima ( ( Fun 𝐹𝑦 ∈ ( 𝐹𝐴 ) ) → ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝑦 )
6 5 ex ( Fun 𝐹 → ( 𝑦 ∈ ( 𝐹𝐴 ) → ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝑦 ) )
7 breq1 ( ( 𝐹𝑥 ) = 𝑦 → ( ( 𝐹𝑥 ) ≼ 𝐵𝑦𝐵 ) )
8 7 biimpd ( ( 𝐹𝑥 ) = 𝑦 → ( ( 𝐹𝑥 ) ≼ 𝐵𝑦𝐵 ) )
9 8 reximi ( ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝑦 → ∃ 𝑥𝐴 ( ( 𝐹𝑥 ) ≼ 𝐵𝑦𝐵 ) )
10 r19.36v ( ∃ 𝑥𝐴 ( ( 𝐹𝑥 ) ≼ 𝐵𝑦𝐵 ) → ( ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵𝑦𝐵 ) )
11 9 10 syl ( ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝑦 → ( ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵𝑦𝐵 ) )
12 6 11 syl6 ( Fun 𝐹 → ( 𝑦 ∈ ( 𝐹𝐴 ) → ( ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵𝑦𝐵 ) ) )
13 12 com23 ( Fun 𝐹 → ( ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵 → ( 𝑦 ∈ ( 𝐹𝐴 ) → 𝑦𝐵 ) ) )
14 13 imp ( ( Fun 𝐹 ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵 ) → ( 𝑦 ∈ ( 𝐹𝐴 ) → 𝑦𝐵 ) )
15 14 ralrimiv ( ( Fun 𝐹 ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵 ) → ∀ 𝑦 ∈ ( 𝐹𝐴 ) 𝑦𝐵 )
16 unidom ( ( ( 𝐹𝐴 ) ∈ V ∧ ∀ 𝑦 ∈ ( 𝐹𝐴 ) 𝑦𝐵 ) → ( 𝐹𝐴 ) ≼ ( ( 𝐹𝐴 ) × 𝐵 ) )
17 4 15 16 syl2anc ( ( Fun 𝐹 ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵 ) → ( 𝐹𝐴 ) ≼ ( ( 𝐹𝐴 ) × 𝐵 ) )
18 imadomg ( 𝐴 ∈ V → ( Fun 𝐹 → ( 𝐹𝐴 ) ≼ 𝐴 ) )
19 1 18 ax-mp ( Fun 𝐹 → ( 𝐹𝐴 ) ≼ 𝐴 )
20 2 xpdom1 ( ( 𝐹𝐴 ) ≼ 𝐴 → ( ( 𝐹𝐴 ) × 𝐵 ) ≼ ( 𝐴 × 𝐵 ) )
21 19 20 syl ( Fun 𝐹 → ( ( 𝐹𝐴 ) × 𝐵 ) ≼ ( 𝐴 × 𝐵 ) )
22 21 adantr ( ( Fun 𝐹 ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵 ) → ( ( 𝐹𝐴 ) × 𝐵 ) ≼ ( 𝐴 × 𝐵 ) )
23 domtr ( ( ( 𝐹𝐴 ) ≼ ( ( 𝐹𝐴 ) × 𝐵 ) ∧ ( ( 𝐹𝐴 ) × 𝐵 ) ≼ ( 𝐴 × 𝐵 ) ) → ( 𝐹𝐴 ) ≼ ( 𝐴 × 𝐵 ) )
24 17 22 23 syl2anc ( ( Fun 𝐹 ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ≼ 𝐵 ) → ( 𝐹𝐴 ) ≼ ( 𝐴 × 𝐵 ) )