iiner

Description: The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015)

		Ref	Expression
	Assertion	iiner	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to ⋂_{x \in A} R Er B$

Proof

Step	Hyp	Ref	Expression
1		r19.2z	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to \exists x \in A R Er B$
2		errel	$⊢ R Er B \to Rel R$
3		df-rel	$⊢ Rel R \leftrightarrow R \subseteq V \times V$
4	2 3	sylib	$⊢ R Er B \to R \subseteq V \times V$
5	4	reximi	$⊢ \exists x \in A R Er B \to \exists x \in A R \subseteq V \times V$
6		iinss	$⊢ \exists x \in A R \subseteq V \times V \to ⋂_{x \in A} R \subseteq V \times V$
7	1 5 6	3syl	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to ⋂_{x \in A} R \subseteq V \times V$
8		df-rel	$⊢ Rel ⋂_{x \in A} R \leftrightarrow ⋂_{x \in A} R \subseteq V \times V$
9	7 8	sylibr	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to Rel ⋂_{x \in A} R$
10		id	$⊢ R Er B \to R Er B$
11	10	ersymb	$⊢ R Er B \to (u R v \leftrightarrow v R u)$
12	11	biimpd	$⊢ R Er B \to (u R v \to v R u)$
13		df-br	$⊢ u R v \leftrightarrow ⟨u, v⟩ \in R$
14		df-br	$⊢ v R u \leftrightarrow ⟨v, u⟩ \in R$
15	12 13 14	3imtr3g	$⊢ R Er B \to (⟨u, v⟩ \in R \to ⟨v, u⟩ \in R)$
16	15	ral2imi	$⊢ \forall x \in A R Er B \to (\forall x \in A ⟨u, v⟩ \in R \to \forall x \in A ⟨v, u⟩ \in R)$
17	16	adantl	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to (\forall x \in A ⟨u, v⟩ \in R \to \forall x \in A ⟨v, u⟩ \in R)$
18		df-br	$⊢ u ⋂_{x \in A} R v \leftrightarrow ⟨u, v⟩ \in ⋂_{x \in A} R$
19		opex	$⊢ ⟨u, v⟩ \in V$
20		eliin	$⊢ ⟨u, v⟩ \in V \to (⟨u, v⟩ \in ⋂_{x \in A} R \leftrightarrow \forall x \in A ⟨u, v⟩ \in R)$
21	19 20	ax-mp	$⊢ ⟨u, v⟩ \in ⋂_{x \in A} R \leftrightarrow \forall x \in A ⟨u, v⟩ \in R$
22	18 21	bitri	$⊢ u ⋂_{x \in A} R v \leftrightarrow \forall x \in A ⟨u, v⟩ \in R$
23		df-br	$⊢ v ⋂_{x \in A} R u \leftrightarrow ⟨v, u⟩ \in ⋂_{x \in A} R$
24		opex	$⊢ ⟨v, u⟩ \in V$
25		eliin	$⊢ ⟨v, u⟩ \in V \to (⟨v, u⟩ \in ⋂_{x \in A} R \leftrightarrow \forall x \in A ⟨v, u⟩ \in R)$
26	24 25	ax-mp	$⊢ ⟨v, u⟩ \in ⋂_{x \in A} R \leftrightarrow \forall x \in A ⟨v, u⟩ \in R$
27	23 26	bitri	$⊢ v ⋂_{x \in A} R u \leftrightarrow \forall x \in A ⟨v, u⟩ \in R$
28	17 22 27	3imtr4g	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to (u ⋂_{x \in A} R v \to v ⋂_{x \in A} R u)$
29	28	imp	$⊢ ((A \neq \emptyset \land \forall x \in A R Er B) \land u ⋂_{x \in A} R v) \to v ⋂_{x \in A} R u$
30		r19.26	$⊢ \forall x \in A (⟨u, v⟩ \in R \land ⟨v, w⟩ \in R) \leftrightarrow (\forall x \in A ⟨u, v⟩ \in R \land \forall x \in A ⟨v, w⟩ \in R)$
31	10	ertr	$⊢ R Er B \to ((u R v \land v R w) \to u R w)$
32		df-br	$⊢ v R w \leftrightarrow ⟨v, w⟩ \in R$
33	13 32	anbi12i	$⊢ (u R v \land v R w) \leftrightarrow (⟨u, v⟩ \in R \land ⟨v, w⟩ \in R)$
34		df-br	$⊢ u R w \leftrightarrow ⟨u, w⟩ \in R$
35	31 33 34	3imtr3g	$⊢ R Er B \to ((⟨u, v⟩ \in R \land ⟨v, w⟩ \in R) \to ⟨u, w⟩ \in R)$
36	35	ral2imi	$⊢ \forall x \in A R Er B \to (\forall x \in A (⟨u, v⟩ \in R \land ⟨v, w⟩ \in R) \to \forall x \in A ⟨u, w⟩ \in R)$
37	36	adantl	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to (\forall x \in A (⟨u, v⟩ \in R \land ⟨v, w⟩ \in R) \to \forall x \in A ⟨u, w⟩ \in R)$
38	30 37	syl5bir	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to ((\forall x \in A ⟨u, v⟩ \in R \land \forall x \in A ⟨v, w⟩ \in R) \to \forall x \in A ⟨u, w⟩ \in R)$
39		df-br	$⊢ v ⋂_{x \in A} R w \leftrightarrow ⟨v, w⟩ \in ⋂_{x \in A} R$
40		opex	$⊢ ⟨v, w⟩ \in V$
41		eliin	$⊢ ⟨v, w⟩ \in V \to (⟨v, w⟩ \in ⋂_{x \in A} R \leftrightarrow \forall x \in A ⟨v, w⟩ \in R)$
42	40 41	ax-mp	$⊢ ⟨v, w⟩ \in ⋂_{x \in A} R \leftrightarrow \forall x \in A ⟨v, w⟩ \in R$
43	39 42	bitri	$⊢ v ⋂_{x \in A} R w \leftrightarrow \forall x \in A ⟨v, w⟩ \in R$
44	22 43	anbi12i	$⊢ (u ⋂_{x \in A} R v \land v ⋂_{x \in A} R w) \leftrightarrow (\forall x \in A ⟨u, v⟩ \in R \land \forall x \in A ⟨v, w⟩ \in R)$
45		df-br	$⊢ u ⋂_{x \in A} R w \leftrightarrow ⟨u, w⟩ \in ⋂_{x \in A} R$
46		opex	$⊢ ⟨u, w⟩ \in V$
47		eliin	$⊢ ⟨u, w⟩ \in V \to (⟨u, w⟩ \in ⋂_{x \in A} R \leftrightarrow \forall x \in A ⟨u, w⟩ \in R)$
48	46 47	ax-mp	$⊢ ⟨u, w⟩ \in ⋂_{x \in A} R \leftrightarrow \forall x \in A ⟨u, w⟩ \in R$
49	45 48	bitri	$⊢ u ⋂_{x \in A} R w \leftrightarrow \forall x \in A ⟨u, w⟩ \in R$
50	38 44 49	3imtr4g	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to ((u ⋂_{x \in A} R v \land v ⋂_{x \in A} R w) \to u ⋂_{x \in A} R w)$
51	50	imp	$⊢ ((A \neq \emptyset \land \forall x \in A R Er B) \land (u ⋂_{x \in A} R v \land v ⋂_{x \in A} R w)) \to u ⋂_{x \in A} R w$
52		simpl	$⊢ (R Er B \land u \in B) \to R Er B$
53		simpr	$⊢ (R Er B \land u \in B) \to u \in B$
54	52 53	erref	$⊢ (R Er B \land u \in B) \to u R u$
55		df-br	$⊢ u R u \leftrightarrow ⟨u, u⟩ \in R$
56	54 55	sylib	$⊢ (R Er B \land u \in B) \to ⟨u, u⟩ \in R$
57	56	expcom	$⊢ u \in B \to (R Er B \to ⟨u, u⟩ \in R)$
58	57	ralimdv	$⊢ u \in B \to (\forall x \in A R Er B \to \forall x \in A ⟨u, u⟩ \in R)$
59	58	com12	$⊢ \forall x \in A R Er B \to (u \in B \to \forall x \in A ⟨u, u⟩ \in R)$
60	59	adantl	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to (u \in B \to \forall x \in A ⟨u, u⟩ \in R)$
61		r19.26	$⊢ \forall x \in A (R Er B \land ⟨u, u⟩ \in R) \leftrightarrow (\forall x \in A R Er B \land \forall x \in A ⟨u, u⟩ \in R)$
62		r19.2z	$⊢ (A \neq \emptyset \land \forall x \in A (R Er B \land ⟨u, u⟩ \in R)) \to \exists x \in A (R Er B \land ⟨u, u⟩ \in R)$
63		vex	$⊢ u \in V$
64	63 63	opeldm	$⊢ ⟨u, u⟩ \in R \to u \in dom R$
65		erdm	$⊢ R Er B \to dom R = B$
66	65	eleq2d	$⊢ R Er B \to (u \in dom R \leftrightarrow u \in B)$
67	66	biimpa	$⊢ (R Er B \land u \in dom R) \to u \in B$
68	64 67	sylan2	$⊢ (R Er B \land ⟨u, u⟩ \in R) \to u \in B$
69	68	rexlimivw	$⊢ \exists x \in A (R Er B \land ⟨u, u⟩ \in R) \to u \in B$
70	62 69	syl	$⊢ (A \neq \emptyset \land \forall x \in A (R Er B \land ⟨u, u⟩ \in R)) \to u \in B$
71	70	ex	$⊢ A \neq \emptyset \to (\forall x \in A (R Er B \land ⟨u, u⟩ \in R) \to u \in B)$
72	61 71	syl5bir	$⊢ A \neq \emptyset \to ((\forall x \in A R Er B \land \forall x \in A ⟨u, u⟩ \in R) \to u \in B)$
73	72	expdimp	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to (\forall x \in A ⟨u, u⟩ \in R \to u \in B)$
74	60 73	impbid	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to (u \in B \leftrightarrow \forall x \in A ⟨u, u⟩ \in R)$
75		df-br	$⊢ u ⋂_{x \in A} R u \leftrightarrow ⟨u, u⟩ \in ⋂_{x \in A} R$
76		opex	$⊢ ⟨u, u⟩ \in V$
77		eliin	$⊢ ⟨u, u⟩ \in V \to (⟨u, u⟩ \in ⋂_{x \in A} R \leftrightarrow \forall x \in A ⟨u, u⟩ \in R)$
78	76 77	ax-mp	$⊢ ⟨u, u⟩ \in ⋂_{x \in A} R \leftrightarrow \forall x \in A ⟨u, u⟩ \in R$
79	75 78	bitri	$⊢ u ⋂_{x \in A} R u \leftrightarrow \forall x \in A ⟨u, u⟩ \in R$
80	74 79	syl6bbr	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to (u \in B \leftrightarrow u ⋂_{x \in A} R u)$
81	9 29 51 80	iserd	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to ⋂_{x \in A} R Er B$

Metamath Proof Explorer

Theorem iiner

Proof