intidl

Description: The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

		Ref	Expression
	Assertion	intidl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∩ 𝐶 ∈ ( Idl ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		intssuni	⊢ ( 𝐶 ≠ ∅ → ∩ 𝐶 ⊆ ∪ 𝐶 )
2	1	3ad2ant2	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∩ 𝐶 ⊆ ∪ 𝐶 )
3		ssel2	⊢ ( ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑖 ∈ 𝐶 ) → 𝑖 ∈ ( Idl ‘ 𝑅 ) )
4		eqid	⊢ ( 1^st ‘ 𝑅 ) = ( 1^st ‘ 𝑅 )
5		eqid	⊢ ran ( 1^st ‘ 𝑅 ) = ran ( 1^st ‘ 𝑅 )
6	4 5	idlss	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → 𝑖 ⊆ ran ( 1^st ‘ 𝑅 ) )
7	3 6	sylan2	⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑖 ∈ 𝐶 ) ) → 𝑖 ⊆ ran ( 1^st ‘ 𝑅 ) )
8	7	anassrs	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝐶 ) → 𝑖 ⊆ ran ( 1^st ‘ 𝑅 ) )
9	8	ralrimiva	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ran ( 1^st ‘ 𝑅 ) )
10	9	3adant2	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ran ( 1^st ‘ 𝑅 ) )
11		unissb	⊢ ( ∪ 𝐶 ⊆ ran ( 1^st ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ran ( 1^st ‘ 𝑅 ) )
12	10 11	sylibr	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∪ 𝐶 ⊆ ran ( 1^st ‘ 𝑅 ) )
13	2 12	sstrd	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∩ 𝐶 ⊆ ran ( 1^st ‘ 𝑅 ) )
14		eqid	⊢ ( GId ‘ ( 1^st ‘ 𝑅 ) ) = ( GId ‘ ( 1^st ‘ 𝑅 ) )
15	4 14	idl0cl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ 𝑖 )
16	3 15	sylan2	⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑖 ∈ 𝐶 ) ) → ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ 𝑖 )
17	16	anassrs	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝐶 ) → ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ 𝑖 )
18	17	ralrimiva	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ 𝑖 )
19		fvex	⊢ ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ V
20	19	elint2	⊢ ( ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ ∩ 𝐶 ↔ ∀ 𝑖 ∈ 𝐶 ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ 𝑖 )
21	18 20	sylibr	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ ∩ 𝐶 )
22	21	3adant2	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ ∩ 𝐶 )
23		vex	⊢ 𝑥 ∈ V
24	23	elint2	⊢ ( 𝑥 ∈ ∩ 𝐶 ↔ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 )
25		vex	⊢ 𝑦 ∈ V
26	25	elint2	⊢ ( 𝑦 ∈ ∩ 𝐶 ↔ ∀ 𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 )
27		r19.26	⊢ ( ∀ 𝑖 ∈ 𝐶 ( 𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖 ) ↔ ( ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ∧ ∀ 𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 ) )
28	4	idladdcl	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖 ) ) → ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 )
29	28	ex	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ( ( 𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖 ) → ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 ) )
30	3 29	sylan2	⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑖 ∈ 𝐶 ) ) → ( ( 𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖 ) → ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 ) )
31	30	anassrs	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖 ) → ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 ) )
32	31	ralimdva	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑖 ∈ 𝐶 ( 𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖 ) → ∀ 𝑖 ∈ 𝐶 ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 ) )
33		ovex	⊢ ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ V
34	33	elint2	⊢ ( ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ↔ ∀ 𝑖 ∈ 𝐶 ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 )
35	32 34	imbitrrdi	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑖 ∈ 𝐶 ( 𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖 ) → ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ) )
36	27 35	biimtrrid	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ( ( ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ∧ ∀ 𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 ) → ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ) )
37	36	expdimp	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) → ( ∀ 𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 → ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ) )
38	26 37	biimtrid	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) → ( 𝑦 ∈ ∩ 𝐶 → ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ) )
39	38	ralrimiv	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) → ∀ 𝑦 ∈ ∩ 𝐶 ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 )
40		eqid	⊢ ( 2^nd ‘ 𝑅 ) = ( 2^nd ‘ 𝑅 )
41	4 40 5	idllmulcl	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝑖 ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ) → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 )
42	41	anass1rs	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑖 ) → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 )
43	42	ex	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 ) )
44	43	an32s	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 ) )
45	3 44	sylan2	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑖 ∈ 𝐶 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 ) )
46	45	an4s	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ∧ 𝑖 ∈ 𝐶 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 ) )
47	46	anassrs	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝐶 ) → ( 𝑥 ∈ 𝑖 → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 ) )
48	47	ralimdva	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) → ( ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 → ∀ 𝑖 ∈ 𝐶 ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 ) )
49	48	imp	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) → ∀ 𝑖 ∈ 𝐶 ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 )
50		ovex	⊢ ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ V
51	50	elint2	⊢ ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ↔ ∀ 𝑖 ∈ 𝐶 ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 )
52	49 51	sylibr	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) → ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 )
53	4 40 5	idlrmulcl	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝑖 ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑖 )
54	53	anass1rs	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑖 ) → ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑖 )
55	54	ex	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑖 ) )
56	55	an32s	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑖 ) )
57	3 56	sylan2	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑖 ∈ 𝐶 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑖 ) )
58	57	an4s	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ∧ 𝑖 ∈ 𝐶 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑖 ) )
59	58	anassrs	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝐶 ) → ( 𝑥 ∈ 𝑖 → ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑖 ) )
60	59	ralimdva	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) → ( ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 → ∀ 𝑖 ∈ 𝐶 ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑖 ) )
61	60	imp	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) → ∀ 𝑖 ∈ 𝐶 ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑖 )
62		ovex	⊢ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ V
63	62	elint2	⊢ ( ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ↔ ∀ 𝑖 ∈ 𝐶 ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑖 )
64	61 63	sylibr	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) → ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 )
65	52 64	jca	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) → ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ) )
66	65	an32s	⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) ∧ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ) → ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ) )
67	66	ralrimiva	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) → ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ) )
68	39 67	jca	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 ) → ( ∀ 𝑦 ∈ ∩ 𝐶 ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ) ) )
69	68	ex	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑖 ∈ 𝐶 𝑥 ∈ 𝑖 → ( ∀ 𝑦 ∈ ∩ 𝐶 ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ) ) ) )
70	24 69	biimtrid	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ( 𝑥 ∈ ∩ 𝐶 → ( ∀ 𝑦 ∈ ∩ 𝐶 ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ) ) ) )
71	70	ralrimiv	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ∩ 𝐶 ( ∀ 𝑦 ∈ ∩ 𝐶 ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ) ) )
72	71	3adant2	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ∩ 𝐶 ( ∀ 𝑦 ∈ ∩ 𝐶 ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ) ) )
73	4 40 5 14	isidl	⊢ ( 𝑅 ∈ RingOps → ( ∩ 𝐶 ∈ ( Idl ‘ 𝑅 ) ↔ ( ∩ 𝐶 ⊆ ran ( 1^st ‘ 𝑅 ) ∧ ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ ∩ 𝐶 ∧ ∀ 𝑥 ∈ ∩ 𝐶 ( ∀ 𝑦 ∈ ∩ 𝐶 ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ) ) ) ) )
74	73	3ad2ant1	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ( ∩ 𝐶 ∈ ( Idl ‘ 𝑅 ) ↔ ( ∩ 𝐶 ⊆ ran ( 1^st ‘ 𝑅 ) ∧ ( GId ‘ ( 1^st ‘ 𝑅 ) ) ∈ ∩ 𝐶 ∧ ∀ 𝑥 ∈ ∩ 𝐶 ( ∀ 𝑦 ∈ ∩ 𝐶 ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝑧 ( 2^nd ‘ 𝑅 ) 𝑥 ) ∈ ∩ 𝐶 ∧ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑧 ) ∈ ∩ 𝐶 ) ) ) ) )
75	13 22 72 74	mpbir3and	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∩ 𝐶 ∈ ( Idl ‘ 𝑅 ) )

Metamath Proof Explorer

Theorem intidl

Proof