Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > konigth | Structured version Visualization version GIF version |
Description: Konig's Theorem. If 𝑚(𝑖) ≺ 𝑛(𝑖) for all 𝑖 ∈ 𝐴, then Σ𝑖 ∈ 𝐴𝑚(𝑖) ≺ ∏𝑖 ∈ 𝐴𝑛(𝑖), 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 𝑚(𝑖) = ∅, 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 |
---|---|
konigth.1 | ⊢ 𝐴 ∈ V |
konigth.2 | ⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) |
konigth.3 | ⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖) |
Ref | Expression |
---|---|
konigth | ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → 𝑆 ≺ 𝑃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | konigth.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | konigth.2 | . 2 ⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖) | |
3 | konigth.3 | . 2 ⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖) | |
4 | fveq2 6675 | . . . . 5 ⊢ (𝑏 = 𝑎 → (𝑓‘𝑏) = (𝑓‘𝑎)) | |
5 | 4 | fveq1d 6677 | . . . 4 ⊢ (𝑏 = 𝑎 → ((𝑓‘𝑏)‘𝑖) = ((𝑓‘𝑎)‘𝑖)) |
6 | 5 | cbvmptv 5134 | . . 3 ⊢ (𝑏 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑏)‘𝑖)) = (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)) |
7 | 6 | mpteq2i 5123 | . 2 ⊢ (𝑖 ∈ 𝐴 ↦ (𝑏 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑏)‘𝑖))) = (𝑖 ∈ 𝐴 ↦ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖))) |
8 | fveq2 6675 | . . 3 ⊢ (𝑗 = 𝑖 → (𝑒‘𝑗) = (𝑒‘𝑖)) | |
9 | 8 | cbvmptv 5134 | . 2 ⊢ (𝑗 ∈ 𝐴 ↦ (𝑒‘𝑗)) = (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖)) |
10 | 1, 2, 3, 7, 9 | konigthlem 10069 | 1 ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → 𝑆 ≺ 𝑃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2113 ∀wral 3053 Vcvv 3398 ∪ ciun 4882 class class class wbr 5031 ↦ cmpt 5111 ‘cfv 6340 Xcixp 8508 ≺ csdm 8555 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5155 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7480 ax-ac2 9964 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3683 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-int 4838 df-iun 4884 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-se 5485 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-pred 6130 df-ord 6176 df-on 6177 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-isom 6349 df-riota 7128 df-ov 7174 df-oprab 7175 df-mpo 7176 df-1st 7715 df-2nd 7716 df-wrecs 7977 df-recs 8038 df-er 8321 df-map 8440 df-ixp 8509 df-en 8557 df-dom 8558 df-sdom 8559 df-card 9442 df-acn 9445 df-ac 9617 |
This theorem is referenced by: pwcfsdom 10084 |
Copyright terms: Public domain | W3C validator |