Theorem konigth

Description: Konig's Theorem. If m ( i ) ~< n ( i ) for all i e. A , then sum_ i e. A m ( i ) ~< prod_ i e. A n ( i ) , where the sums and products stand in for disjoint union and infinite cartesian product. The version here is proven with unions rather than disjoint unions for convenience, but the version with disjoint unions is clearly a special case of this version. The Axiom of Choice is needed for this proof, but it contains AC as a simple corollary (letting m ( i ) = (/) , this theorem says that an infinite cartesian product of nonempty sets is nonempty), so this is an AC equivalent. Theorem 11.26 of TakeutiZaring p. 107. (Contributed by Mario Carneiro, 22-Feb-2013)

	Ref	Expression
Hypotheses	konigth.1	⊢ 𝐴 ∈ V
	konigth.2	⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 )
	konigth.3	⊢ 𝑃 = X 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 )
Assertion	konigth	⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → 𝑆 ≺ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		konigth.1	⊢ 𝐴 ∈ V
2		konigth.2	⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 )
3		konigth.3	⊢ 𝑃 = X 𝑖 ∈ 𝐴 ( 𝑁 ‘ 𝑖 )
4		fveq2	⊢ ( 𝑏 = 𝑎 → ( 𝑓 ‘ 𝑏 ) = ( 𝑓 ‘ 𝑎 ) )
5	4	fveq1d	⊢ ( 𝑏 = 𝑎 → ( ( 𝑓 ‘ 𝑏 ) ‘ 𝑖 ) = ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) )
6	5	cbvmptv	⊢ ( 𝑏 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑏 ) ‘ 𝑖 ) ) = ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) )
7	6	mpteq2i	⊢ ( 𝑖 ∈ 𝐴 ↦ ( 𝑏 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑏 ) ‘ 𝑖 ) ) ) = ( 𝑖 ∈ 𝐴 ↦ ( 𝑎 ∈ ( 𝑀 ‘ 𝑖 ) ↦ ( ( 𝑓 ‘ 𝑎 ) ‘ 𝑖 ) ) )
8		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝑒 ‘ 𝑗 ) = ( 𝑒 ‘ 𝑖 ) )
9	8	cbvmptv	⊢ ( 𝑗 ∈ 𝐴 ↦ ( 𝑒 ‘ 𝑗 ) ) = ( 𝑖 ∈ 𝐴 ↦ ( 𝑒 ‘ 𝑖 ) )
10	1 2 3 7 9	konigthlem	⊢ ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) ≺ ( 𝑁 ‘ 𝑖 ) → 𝑆 ≺ 𝑃 )