ssdifidllem - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ssdifidllem		Structured version Visualization version GIF version

Theorem ssdifidllem 33411

Description: Lemma for ssdifidl 33412: The set 𝑃 used in the proof of ssdifidl 33412 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 3-Jun-2025.)

**Hypotheses**
Ref	Expression
ssdifidl.1	⊢ 𝐵 = (Base‘𝑅)
ssdifidl.2	⊢ (𝜑 → 𝑅 ∈ Ring)
ssdifidl.3	⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))
ssdifidl.4	⊢ (𝜑 → 𝑆 ⊆ 𝐵)
ssdifidl.5	⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅)
ssdifidl.6	⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}
ssdifidllem.7	⊢ (𝜑 → 𝑍 ⊆ 𝑃)
ssdifidllem.8	⊢ (𝜑 → 𝑍 ≠ ∅)
ssdifidllem.9	⊢ (𝜑 → [⊊] Or 𝑍)

**Assertion**
Ref	Expression
ssdifidllem	⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃)

Distinct variable groups: 𝐼,𝑝 𝑅,𝑝 𝑆,𝑝 𝑍,𝑝 Allowed substitution hints: 𝜑(𝑝) 𝐵(𝑝) 𝑃(𝑝)

Proof of Theorem ssdifidllem Dummy variables 𝑎 𝑏 𝑖 𝑗 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ineq2 4162	. . . . 5 ⊢ (𝑝 = ∪ 𝑍 → (𝑆 ∩ 𝑝) = (𝑆 ∩ ∪ 𝑍))
2	1	eqeq1d 2732	. . . 4 ⊢ (𝑝 = ∪ 𝑍 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑆 ∩ ∪ 𝑍) = ∅))
3		sseq2 3959	. . . 4 ⊢ (𝑝 = ∪ 𝑍 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ ∪ 𝑍))
4	2, 3	anbi12d 632	. . 3 ⊢ (𝑝 = ∪ 𝑍 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑆 ∩ ∪ 𝑍) = ∅ ∧ 𝐼 ⊆ ∪ 𝑍)))
5		ssdifidllem.7	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ⊆ 𝑃)
6		ssdifidl.6	. . . . . . . . . 10 ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}
7	6	ssrab3 4030	. . . . . . . . 9 ⊢ 𝑃 ⊆ (LIdeal‘𝑅)
8	5, 7	sstrdi 3945	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ⊆ (LIdeal‘𝑅))
9	8	sselda 3932	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (LIdeal‘𝑅))
10		ssdifidl.1	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑅)
11		eqid 2730	. . . . . . . 8 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
12	10, 11	lidlss 21142	. . . . . . 7 ⊢ (𝑗 ∈ (LIdeal‘𝑅) → 𝑗 ⊆ 𝐵)
13	9, 12	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ⊆ 𝐵)
14	13	ralrimiva 3122	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 𝑗 ⊆ 𝐵)
15		unissb 4889	. . . . 5 ⊢ (∪ 𝑍 ⊆ 𝐵 ↔ ∀𝑗 ∈ 𝑍 𝑗 ⊆ 𝐵)
16	14, 15	sylibr 234	. . . 4 ⊢ (𝜑 → ∪ 𝑍 ⊆ 𝐵)
17		ssdifidllem.8	. . . . . . 7 ⊢ (𝜑 → 𝑍 ≠ ∅)
18		ssdifidl.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Ring)
19		eqid 2730	. . . . . . . . . . 11 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
20	11, 19	lidl0cl 21150	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) → (0_g‘𝑅) ∈ 𝑗)
21	18, 9, 20	syl2an2r 685	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (0_g‘𝑅) ∈ 𝑗)
22		n0i 4288	. . . . . . . . 9 ⊢ ((0_g‘𝑅) ∈ 𝑗 → ¬ 𝑗 = ∅)
23	21, 22	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ¬ 𝑗 = ∅)
24	23	reximdva0 4303	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 ≠ ∅) → ∃𝑗 ∈ 𝑍 ¬ 𝑗 = ∅)
25	17, 24	mpdan 687	. . . . . 6 ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ¬ 𝑗 = ∅)
26		rexnal 3082	. . . . . 6 ⊢ (∃𝑗 ∈ 𝑍 ¬ 𝑗 = ∅ ↔ ¬ ∀𝑗 ∈ 𝑍 𝑗 = ∅)
27	25, 26	sylib 218	. . . . 5 ⊢ (𝜑 → ¬ ∀𝑗 ∈ 𝑍 𝑗 = ∅)
28		uni0c 4884	. . . . . 6 ⊢ (∪ 𝑍 = ∅ ↔ ∀𝑗 ∈ 𝑍 𝑗 = ∅)
29	28	necon3abii 2972	. . . . 5 ⊢ (∪ 𝑍 ≠ ∅ ↔ ¬ ∀𝑗 ∈ 𝑍 𝑗 = ∅)
30	27, 29	sylibr 234	. . . 4 ⊢ (𝜑 → ∪ 𝑍 ≠ ∅)
31		eluni2 4861	. . . . . . . 8 ⊢ (𝑎 ∈ ∪ 𝑍 ↔ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖)
32		eluni2 4861	. . . . . . . 8 ⊢ (𝑏 ∈ ∪ 𝑍 ↔ ∃𝑗 ∈ 𝑍 𝑏 ∈ 𝑗)
33	31, 32	anbi12i 628	. . . . . . 7 ⊢ ((𝑎 ∈ ∪ 𝑍 ∧ 𝑏 ∈ ∪ 𝑍) ↔ (∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖 ∧ ∃𝑗 ∈ 𝑍 𝑏 ∈ 𝑗))
34		an32 646	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖) ∧ 𝑗 ∈ 𝑍) ↔ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖))
35	18	ad6antr 736	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑅 ∈ Ring)
36	8	ad6antr 736	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑍 ⊆ (LIdeal‘𝑅))
37		simp-5r 785	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑗 ∈ 𝑍)
38	36, 37	sseldd 3933	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑗 ∈ (LIdeal‘𝑅))
39		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (._r‘𝑅) = (._r‘𝑅)
40		simp-6r 787	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑥 ∈ 𝐵)
41		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑖 ⊆ 𝑗)
42		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑎 ∈ 𝑖)
43	41, 42	sseldd 3933	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑎 ∈ 𝑗)
44	11, 10, 39, 35, 38, 40, 43	lidlmcld 33374	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → (𝑥(._r‘𝑅)𝑎) ∈ 𝑗)
45		simp-4r 783	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → 𝑏 ∈ 𝑗)
46		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
47	11, 46	lidlacl 21151	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(._r‘𝑅)𝑎) ∈ 𝑗 ∧ 𝑏 ∈ 𝑗)) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ 𝑗)
48	35, 38, 44, 45, 47	syl22anc 838	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ 𝑗)
49		elunii 4862	. . . . . . . . . . . . . 14 ⊢ ((((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ 𝑗 ∧ 𝑗 ∈ 𝑍) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
50	48, 37, 49	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑗) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
51	18	ad6antr 736	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑅 ∈ Ring)
52	8	ad6antr 736	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑍 ⊆ (LIdeal‘𝑅))
53		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑖 ∈ 𝑍)
54	52, 53	sseldd 3933	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
55		simp-6r 787	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑥 ∈ 𝐵)
56		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑎 ∈ 𝑖)
57	11, 10, 39, 51, 54, 55, 56	lidlmcld 33374	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → (𝑥(._r‘𝑅)𝑎) ∈ 𝑖)
58		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑗 ⊆ 𝑖)
59		simp-4r 783	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑏 ∈ 𝑗)
60	58, 59	sseldd 3933	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → 𝑏 ∈ 𝑖)
61	11, 46	lidlacl 21151	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(._r‘𝑅)𝑎) ∈ 𝑖 ∧ 𝑏 ∈ 𝑖)) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ 𝑖)
62	51, 54, 57, 60, 61	syl22anc 838	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ 𝑖)
63		elunii 4862	. . . . . . . . . . . . . 14 ⊢ ((((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ 𝑖 ∧ 𝑖 ∈ 𝑍) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
64	62, 53, 63	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) ∧ 𝑗 ⊆ 𝑖) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
65		ssdifidllem.9	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → [⊊] Or 𝑍)
66	65	ad5antr 734	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → [⊊] Or 𝑍)
67		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → 𝑖 ∈ 𝑍)
68		simp-4r 783	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → 𝑗 ∈ 𝑍)
69		sorpssi 7657	. . . . . . . . . . . . . 14 ⊢ (( [⊊] Or 𝑍 ∧ (𝑖 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍)) → (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))
70	66, 67, 68, 69	syl12anc 836	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))
71	50, 64, 70	mpjaodan 960	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ 𝑎 ∈ 𝑖) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
72	71	r19.29an 3134	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
73	72	an32s 652	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑗 ∈ 𝑍) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖) ∧ 𝑏 ∈ 𝑗) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
74	34, 73	sylanb 581	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
75	74	r19.29an 3134	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖) ∧ ∃𝑗 ∈ 𝑍 𝑏 ∈ 𝑗) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
76	75	anasss 466	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (∃𝑖 ∈ 𝑍 𝑎 ∈ 𝑖 ∧ ∃𝑗 ∈ 𝑍 𝑏 ∈ 𝑗)) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
77	33, 76	sylan2b 594	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑎 ∈ ∪ 𝑍 ∧ 𝑏 ∈ ∪ 𝑍)) → ((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
78	77	ralrimivva 3173	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑎 ∈ ∪ 𝑍∀𝑏 ∈ ∪ 𝑍((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
79	78	ralrimiva 3122	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ ∪ 𝑍∀𝑏 ∈ ∪ 𝑍((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍)
80	11, 10, 46, 39	islidl 21145	. . . 4 ⊢ (∪ 𝑍 ∈ (LIdeal‘𝑅) ↔ (∪ 𝑍 ⊆ 𝐵 ∧ ∪ 𝑍 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑎 ∈ ∪ 𝑍∀𝑏 ∈ ∪ 𝑍((𝑥(._r‘𝑅)𝑎)(+_g‘𝑅)𝑏) ∈ ∪ 𝑍))
81	16, 30, 79, 80	syl3anbrc 1344	. . 3 ⊢ (𝜑 → ∪ 𝑍 ∈ (LIdeal‘𝑅))
82		iunss1 4954	. . . . . . 7 ⊢ (𝑍 ⊆ 𝑃 → ∪ 𝑗 ∈ 𝑍 (𝑆 ∩ 𝑗) ⊆ ∪ 𝑗 ∈ 𝑃 (𝑆 ∩ 𝑗))
83	5, 82	syl 17	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝑍 (𝑆 ∩ 𝑗) ⊆ ∪ 𝑗 ∈ 𝑃 (𝑆 ∩ 𝑗))
84		uniin2 32522	. . . . . . 7 ⊢ ∪ 𝑗 ∈ 𝑍 (𝑆 ∩ 𝑗) = (𝑆 ∩ ∪ 𝑍)
85	84	a1i 11	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝑍 (𝑆 ∩ 𝑗) = (𝑆 ∩ ∪ 𝑍))
86	7	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ⊆ (LIdeal‘𝑅))
87	86	sselda 3932	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑃) → 𝑗 ∈ (LIdeal‘𝑅))
88		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑃) → 𝑗 ∈ 𝑃)
89	88, 6	eleqtrdi 2839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑃) → 𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)})
90		ineq2 4162	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑗 → (𝑆 ∩ 𝑝) = (𝑆 ∩ 𝑗))
91	90	eqeq1d 2732	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑗 → ((𝑆 ∩ 𝑝) = ∅ ↔ (𝑆 ∩ 𝑗) = ∅))
92		sseq2 3959	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑗 → (𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑗))
93	91, 92	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑗 → (((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝) ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
94	93	elrab3 3646	. . . . . . . . . 10 ⊢ (𝑗 ∈ (LIdeal‘𝑅) → (𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)} ↔ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
95	94	simprbda 498	. . . . . . . . 9 ⊢ ((𝑗 ∈ (LIdeal‘𝑅) ∧ 𝑗 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)}) → (𝑆 ∩ 𝑗) = ∅)
96	87, 89, 95	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑃) → (𝑆 ∩ 𝑗) = ∅)
97	96	iuneq2dv 4964	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝑃 (𝑆 ∩ 𝑗) = ∪ 𝑗 ∈ 𝑃 ∅)
98		iun0 5008	. . . . . . 7 ⊢ ∪ 𝑗 ∈ 𝑃 ∅ = ∅
99	97, 98	eqtrdi 2781	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝑃 (𝑆 ∩ 𝑗) = ∅)
100	83, 85, 99	3sstr3d 3987	. . . . 5 ⊢ (𝜑 → (𝑆 ∩ ∪ 𝑍) ⊆ ∅)
101		ss0 4350	. . . . 5 ⊢ ((𝑆 ∩ ∪ 𝑍) ⊆ ∅ → (𝑆 ∩ ∪ 𝑍) = ∅)
102	100, 101	syl 17	. . . 4 ⊢ (𝜑 → (𝑆 ∩ ∪ 𝑍) = ∅)
103	5	sselda 3932	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑃)
104	93, 6	elrab2 3648	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
105	103, 104	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 ∈ (LIdeal‘𝑅) ∧ ((𝑆 ∩ 𝑗) = ∅ ∧ 𝐼 ⊆ 𝑗)))
106	105	simprrd 773	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐼 ⊆ 𝑗)
107	106	ralrimiva 3122	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 𝐼 ⊆ 𝑗)
108		ssint 4912	. . . . . 6 ⊢ (𝐼 ⊆ ∩ 𝑍 ↔ ∀𝑗 ∈ 𝑍 𝐼 ⊆ 𝑗)
109	107, 108	sylibr 234	. . . . 5 ⊢ (𝜑 → 𝐼 ⊆ ∩ 𝑍)
110		intssuni 4918	. . . . . 6 ⊢ (𝑍 ≠ ∅ → ∩ 𝑍 ⊆ ∪ 𝑍)
111	17, 110	syl 17	. . . . 5 ⊢ (𝜑 → ∩ 𝑍 ⊆ ∪ 𝑍)
112	109, 111	sstrd 3943	. . . 4 ⊢ (𝜑 → 𝐼 ⊆ ∪ 𝑍)
113	102, 112	jca 511	. . 3 ⊢ (𝜑 → ((𝑆 ∩ ∪ 𝑍) = ∅ ∧ 𝐼 ⊆ ∪ 𝑍))
114	4, 81, 113	elrabd 3647	. 2 ⊢ (𝜑 → ∪ 𝑍 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)})
115	114, 6	eleqtrrdi 2840	1 ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2110 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 {crab 3393 ∩ cin 3899 ⊆ wss 3900 ∅c0 4281 ∪ cuni 4857 ∩ cint 4895 ∪ ciun 4939 Or wor 5521 ‘cfv 6477 (class class class)co 7341 [⊊] crpss 7650 Basecbs 17112 +_gcplusg 17153 ._rcmulr 17154 0_gc0g 17335 Ringcrg 20144 LIdealclidl 21136

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-cnex 11054 ax-resscn 11055 ax-1cn 11056 ax-icn 11057 ax-addcl 11058 ax-addrcl 11059 ax-mulcl 11060 ax-mulrcl 11061 ax-mulcom 11062 ax-addass 11063 ax-mulass 11064 ax-distr 11065 ax-i2m1 11066 ax-1ne0 11067 ax-1rid 11068 ax-rnegex 11069 ax-rrecex 11070 ax-cnre 11071 ax-pre-lttri 11072 ax-pre-lttrn 11073 ax-pre-ltadd 11074 ax-pre-mulgt0 11075

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3344 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6244 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-rpss 7651 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-pnf 11140 df-mnf 11141 df-xr 11142 df-ltxr 11143 df-le 11144 df-sub 11338 df-neg 11339 df-nn 12118 df-2 12180 df-3 12181 df-4 12182 df-5 12183 df-6 12184 df-7 12185 df-8 12186 df-sets 17067 df-slot 17085 df-ndx 17097 df-base 17113 df-ress 17134 df-plusg 17166 df-mulr 17167 df-sca 17169 df-vsca 17170 df-ip 17171 df-0g 17337 df-mgm 18540 df-sgrp 18619 df-mnd 18635 df-grp 18841 df-minusg 18842 df-sbg 18843 df-subg 19028 df-cmn 19687 df-abl 19688 df-mgp 20052 df-rng 20064 df-ur 20093 df-ring 20146 df-subrg 20478 df-lmod 20788 df-lss 20858 df-sra 21100 df-rgmod 21101 df-lidl 21138

This theorem is referenced by: ssdifidl 33412

W3C validator