![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpen | Structured version Visualization version GIF version |
Description: Equinumerosity law for Cartesian product. Proposition 4.22(b) of [Mendelson] p. 254. (Contributed by NM, 24-Jul-2004.) (Proof shortened by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
xpen | ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 × 𝐶) ≈ (𝐵 × 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relen 8309 | . . . . 5 ⊢ Rel ≈ | |
2 | 1 | brrelex1i 5454 | . . . 4 ⊢ (𝐶 ≈ 𝐷 → 𝐶 ∈ V) |
3 | endom 8331 | . . . 4 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) | |
4 | xpdom1g 8408 | . . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐴 ≼ 𝐵) → (𝐴 × 𝐶) ≼ (𝐵 × 𝐶)) | |
5 | 2, 3, 4 | syl2anr 587 | . . 3 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 × 𝐶) ≼ (𝐵 × 𝐶)) |
6 | 1 | brrelex2i 5455 | . . . 4 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ∈ V) |
7 | endom 8331 | . . . 4 ⊢ (𝐶 ≈ 𝐷 → 𝐶 ≼ 𝐷) | |
8 | xpdom2g 8407 | . . . 4 ⊢ ((𝐵 ∈ V ∧ 𝐶 ≼ 𝐷) → (𝐵 × 𝐶) ≼ (𝐵 × 𝐷)) | |
9 | 6, 7, 8 | syl2an 586 | . . 3 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐵 × 𝐶) ≼ (𝐵 × 𝐷)) |
10 | domtr 8357 | . . 3 ⊢ (((𝐴 × 𝐶) ≼ (𝐵 × 𝐶) ∧ (𝐵 × 𝐶) ≼ (𝐵 × 𝐷)) → (𝐴 × 𝐶) ≼ (𝐵 × 𝐷)) | |
11 | 5, 9, 10 | syl2anc 576 | . 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 × 𝐶) ≼ (𝐵 × 𝐷)) |
12 | 1 | brrelex2i 5455 | . . . 4 ⊢ (𝐶 ≈ 𝐷 → 𝐷 ∈ V) |
13 | ensym 8353 | . . . . 5 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | |
14 | endom 8331 | . . . . 5 ⊢ (𝐵 ≈ 𝐴 → 𝐵 ≼ 𝐴) | |
15 | 13, 14 | syl 17 | . . . 4 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≼ 𝐴) |
16 | xpdom1g 8408 | . . . 4 ⊢ ((𝐷 ∈ V ∧ 𝐵 ≼ 𝐴) → (𝐵 × 𝐷) ≼ (𝐴 × 𝐷)) | |
17 | 12, 15, 16 | syl2anr 587 | . . 3 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐵 × 𝐷) ≼ (𝐴 × 𝐷)) |
18 | 1 | brrelex1i 5454 | . . . 4 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ∈ V) |
19 | ensym 8353 | . . . . 5 ⊢ (𝐶 ≈ 𝐷 → 𝐷 ≈ 𝐶) | |
20 | endom 8331 | . . . . 5 ⊢ (𝐷 ≈ 𝐶 → 𝐷 ≼ 𝐶) | |
21 | 19, 20 | syl 17 | . . . 4 ⊢ (𝐶 ≈ 𝐷 → 𝐷 ≼ 𝐶) |
22 | xpdom2g 8407 | . . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐷 ≼ 𝐶) → (𝐴 × 𝐷) ≼ (𝐴 × 𝐶)) | |
23 | 18, 21, 22 | syl2an 586 | . . 3 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 × 𝐷) ≼ (𝐴 × 𝐶)) |
24 | domtr 8357 | . . 3 ⊢ (((𝐵 × 𝐷) ≼ (𝐴 × 𝐷) ∧ (𝐴 × 𝐷) ≼ (𝐴 × 𝐶)) → (𝐵 × 𝐷) ≼ (𝐴 × 𝐶)) | |
25 | 17, 23, 24 | syl2anc 576 | . 2 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐵 × 𝐷) ≼ (𝐴 × 𝐶)) |
26 | sbth 8431 | . 2 ⊢ (((𝐴 × 𝐶) ≼ (𝐵 × 𝐷) ∧ (𝐵 × 𝐷) ≼ (𝐴 × 𝐶)) → (𝐴 × 𝐶) ≈ (𝐵 × 𝐷)) | |
27 | 11, 25, 26 | syl2anc 576 | 1 ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 × 𝐶) ≈ (𝐵 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2050 Vcvv 3409 class class class wbr 4925 × cxp 5401 ≈ cen 8301 ≼ cdom 8302 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-1st 7499 df-2nd 7500 df-er 8087 df-en 8305 df-dom 8306 |
This theorem is referenced by: map2xp 8481 unxpdom2 8519 sucxpdom 8520 xpnum 9172 infxpenlem 9231 infxpidm2 9235 xpdjuen 9401 mapdjuen 9402 pwdjuen 9403 djuxpdom 9407 ackbij1lem5 9442 canthp1lem1 9870 xpnnen 15422 qnnen 15424 rexpen 15439 met2ndci 22847 re2ndc 23124 dyadmbl 23916 opnmblALT 23919 mbfimaopnlem 23971 mblfinlem1 34399 |
Copyright terms: Public domain | W3C validator |