Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > paddssat | Structured version Visualization version GIF version |
Description: A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012.) |
Ref | Expression |
---|---|
padd0.a | ⊢ 𝐴 = (Atoms‘𝐾) |
padd0.p | ⊢ + = (+𝑃‘𝐾) |
Ref | Expression |
---|---|
paddssat | ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . . 3 ⊢ (le‘𝐾) = (le‘𝐾) | |
2 | eqid 2738 | . . 3 ⊢ (join‘𝐾) = (join‘𝐾) | |
3 | padd0.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | padd0.p | . . 3 ⊢ + = (+𝑃‘𝐾) | |
5 | 1, 2, 3, 4 | paddval 37579 | . 2 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)})) |
6 | unss 4113 | . . . . . 6 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ↔ (𝑋 ∪ 𝑌) ⊆ 𝐴) | |
7 | 6 | biimpi 219 | . . . . 5 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ∪ 𝑌) ⊆ 𝐴) |
8 | ssrab2 4008 | . . . . 5 ⊢ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)} ⊆ 𝐴 | |
9 | 7, 8 | jctir 524 | . . . 4 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ∪ 𝑌) ⊆ 𝐴 ∧ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)} ⊆ 𝐴)) |
10 | unss 4113 | . . . 4 ⊢ (((𝑋 ∪ 𝑌) ⊆ 𝐴 ∧ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)} ⊆ 𝐴) ↔ ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)}) ⊆ 𝐴) | |
11 | 9, 10 | sylib 221 | . . 3 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)}) ⊆ 𝐴) |
12 | 11 | 3adant1 1132 | . 2 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)}) ⊆ 𝐴) |
13 | 5, 12 | eqsstrd 3954 | 1 ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2111 ∃wrex 3063 {crab 3066 ∪ cun 3879 ⊆ wss 3881 class class class wbr 5068 ‘cfv 6398 (class class class)co 7232 lecple 16837 joincjn 17846 Atomscatm 37044 +𝑃cpadd 37576 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-rep 5194 ax-sep 5207 ax-nul 5214 ax-pow 5273 ax-pr 5337 ax-un 7542 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ne 2942 df-ral 3067 df-rex 3068 df-reu 3069 df-rab 3071 df-v 3423 df-sbc 3710 df-csb 3827 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4253 df-if 4455 df-pw 4530 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4835 df-iun 4921 df-br 5069 df-opab 5131 df-mpt 5151 df-id 5470 df-xp 5572 df-rel 5573 df-cnv 5574 df-co 5575 df-dm 5576 df-rn 5577 df-res 5578 df-ima 5579 df-iota 6356 df-fun 6400 df-fn 6401 df-f 6402 df-f1 6403 df-fo 6404 df-f1o 6405 df-fv 6406 df-ov 7235 df-oprab 7236 df-mpo 7237 df-1st 7780 df-2nd 7781 df-padd 37577 |
This theorem is referenced by: paddasslem8 37608 paddasslem11 37611 paddasslem12 37612 paddasslem13 37613 paddasslem16 37616 paddasslem17 37617 paddass 37619 padd4N 37621 paddclN 37623 pmodl42N 37632 pclunN 37679 paddunN 37708 pmapocjN 37711 pclfinclN 37731 osumcllem1N 37737 osumcllem2N 37738 osumcllem9N 37745 osumcllem11N 37747 osumclN 37748 pexmidlem6N 37756 pexmidlem8N 37758 pl42lem3N 37762 |
Copyright terms: Public domain | W3C validator |