uninqs - User Sandbox

User Sandbox

< Previous Next >
Related theorems
GIF version

Theorem uninqs 10436

Description: The class union of the intersection of two subclasses of a quotient space. Compare uniin 2524.

**Hypothesis**
Ref	Expression
uninqs.1	⊢ Er R

**Assertion**
Ref	Expression
uninqs	⊢ ((B ⊆ (A / R) ⋀ C ⊆ (A / R)) → ∪(B ∩ C) = (∪B ∩ ∪C))

**Proof of Theorem uninqs**
Step	Hyp	Ref	Expression
1		dfss2 2061	. . . . . . . . . . . . . . 15 ⊢ (B ⊆ (A / R) ↔ ∀b(b ∈ B → b ∈ (A / R)))
2		dfss2 2061	. . . . . . . . . . . . . . . . . 18 ⊢ (C ⊆ (A / R) ↔ ∀a(a ∈ C → a ∈ (A / R)))
3		pm3.35 359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((a ∈ C ⋀ (a ∈ C → a ∈ (A / R))) → a ∈ (A / R))
4		pm3.35 359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((b ∈ B ⋀ (b ∈ B → b ∈ (A / R))) → b ∈ (A / R))
5		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ b ∈ V
6	5	elqs 4296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (b ∈ (A / R) ↔ ∃u(u ∈ A ⋀ b = [u]R))
7		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ a ∈ V
8	7	elqs 4296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (a ∈ (A / R) ↔ ∃v(v ∈ A ⋀ a = [v]R))
9		inelcm 2327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 ⊢ ((x ∈ [v]R ⋀ x ∈ [u]R) → ([v]R ∩ [u]R) ≠ ∅)
10		df-ne 1590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 ⊢ (([v]R ∩ [u]R) ≠ ∅ ↔ ¬ ([v]R ∩ [u]R) = ∅)
11		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 ⊢ v ∈ V
12		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 ⊢ u ∈ V
13		uninqs.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 ⊢ Er R
14	11, 12, 13	erdisj 4292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 ⊢ ([v]R = [u]R ⋁ ([v]R ∩ [u]R) = ∅)
15		pm5.61 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 ⊢ ((([v]R = [u]R ⋁ ([v]R ∩ [u]R) = ∅) ⋀ ¬ ([v]R ∩ [u]R) = ∅) ↔ ([v]R = [u]R ⋀ ¬ ([v]R ∩ [u]R) = ∅))
16		eqeq12 1490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 ⊢ ((a = [v]R ⋀ b = [u]R) → (a = b ↔ [v]R = [u]R))
17	16	biimprcd 156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 ⊢ ([v]R = [u]R → ((a = [v]R ⋀ b = [u]R) → a = b))
18	17	adantr 391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 ⊢ (([v]R = [u]R ⋀ ¬ ([v]R ∩ [u]R) = ∅) → ((a = [v]R ⋀ b = [u]R) → a = b))
19	15, 18	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 ⊢ ((([v]R = [u]R ⋁ ([v]R ∩ [u]R) = ∅) ⋀ ¬ ([v]R ∩ [u]R) = ∅) → ((a = [v]R ⋀ b = [u]R) → a = b))
20	14, 19	mpan 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 ⊢ (¬ ([v]R ∩ [u]R) = ∅ → ((a = [v]R ⋀ b = [u]R) → a = b))
21	10, 20	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 ⊢ (([v]R ∩ [u]R) ≠ ∅ → ((a = [v]R ⋀ b = [u]R) → a = b))
22	9, 21	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 ⊢ ((x ∈ [v]R ⋀ x ∈ [u]R) → ((a = [v]R ⋀ b = [u]R) → a = b))
23		eleq2 1538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 ⊢ (a = [v]R → (x ∈ a ↔ x ∈ [v]R))
24	23	biimpa 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 ⊢ ((a = [v]R ⋀ x ∈ a) → x ∈ [v]R)
25		eleq2 1538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 ⊢ (b = [u]R → (x ∈ b ↔ x ∈ [u]R))
26	25	biimpa 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 ⊢ ((b = [u]R ⋀ x ∈ b) → x ∈ [u]R)
27	22, 24, 26	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 ⊢ (((a = [v]R ⋀ x ∈ a) ⋀ (b = [u]R ⋀ x ∈ b)) → ((a = [v]R ⋀ b = [u]R) → a = b))
28	27	an4s 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 ⊢ (((a = [v]R ⋀ b = [u]R) ⋀ (x ∈ a ⋀ x ∈ b)) → ((a = [v]R ⋀ b = [u]R) → a = b))
29	28	exp32 379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 ⊢ ((a = [v]R ⋀ b = [u]R) → (x ∈ a → (x ∈ b → ((a = [v]R ⋀ b = [u]R) → a = b))))
30	29	com24 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 ⊢ ((a = [v]R ⋀ b = [u]R) → ((a = [v]R ⋀ b = [u]R) → (x ∈ b → (x ∈ a → a = b))))
31	30	pm2.43i 64	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 ⊢ ((a = [v]R ⋀ b = [u]R) → (x ∈ b → (x ∈ a → a = b)))
32	31	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 ⊢ (a = [v]R → (b = [u]R → (x ∈ b → (x ∈ a → a = b))))
33	32	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 ⊢ ((v ∈ A ⋀ a = [v]R) → (b = [u]R → (x ∈ b → (x ∈ a → a = b))))
34	33	19.23aiv 1297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 ⊢ (∃v(v ∈ A ⋀ a = [v]R) → (b = [u]R → (x ∈ b → (x ∈ a → a = b))))
35	8, 34	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 ⊢ (a ∈ (A / R) → (b = [u]R → (x ∈ b → (x ∈ a → a = b))))
36	35	com3l 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (b = [u]R → (x ∈ b → (a ∈ (A / R) → (x ∈ a → a = b))))
37	36	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ ((u ∈ A ⋀ b = [u]R) → (x ∈ b → (a ∈ (A / R) → (x ∈ a → a = b))))
38	37	19.23aiv 1297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (∃u(u ∈ A ⋀ b = [u]R) → (x ∈ b → (a ∈ (A / R) → (x ∈ a → a = b))))
39	6, 38	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (b ∈ (A / R) → (x ∈ b → (a ∈ (A / R) → (x ∈ a → a = b))))
40	4, 39	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((b ∈ B ⋀ (b ∈ B → b ∈ (A / R))) → (x ∈ b → (a ∈ (A / R) → (x ∈ a → a = b))))
41	40	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (b ∈ B → ((b ∈ B → b ∈ (A / R)) → (x ∈ b → (a ∈ (A / R) → (x ∈ a → a = b)))))
42	41	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (b ∈ B → (x ∈ b → ((b ∈ B → b ∈ (A / R)) → (a ∈ (A / R) → (x ∈ a → a = b)))))
43	42	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((b ∈ B ⋀ x ∈ b) → ((b ∈ B → b ∈ (A / R)) → (a ∈ (A / R) → (x ∈ a → a = b))))
44	43	com13 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (a ∈ (A / R) → ((b ∈ B → b ∈ (A / R)) → ((b ∈ B ⋀ x ∈ b) → (x ∈ a → a = b))))
45	3, 44	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((a ∈ C ⋀ (a ∈ C → a ∈ (A / R))) → ((b ∈ B → b ∈ (A / R)) → ((b ∈ B ⋀ x ∈ b) → (x ∈ a → a = b))))
46	45	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (a ∈ C → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ((b ∈ B ⋀ x ∈ b) → (x ∈ a → a = b)))))
47	46	com24 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (a ∈ C → ((b ∈ B ⋀ x ∈ b) → ((b ∈ B → b ∈ (A / R)) → ((a ∈ C → a ∈ (A / R)) → (x ∈ a → a = b)))))
48	47	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((a ∈ C ⋀ (b ∈ B ⋀ x ∈ b)) → ((b ∈ B → b ∈ (A / R)) → ((a ∈ C → a ∈ (A / R)) → (x ∈ a → a = b))))
49	48	com24 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((a ∈ C ⋀ (b ∈ B ⋀ x ∈ b)) → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → a = b))))
50	49	imp31 362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((a ∈ C ⋀ (b ∈ B ⋀ x ∈ b)) ⋀ x ∈ a) ⋀ (a ∈ C → a ∈ (A / R))) → ((b ∈ B → b ∈ (A / R)) → a = b))
51		eleq1 1537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (a = b → (a ∈ C ↔ b ∈ C))
52		elin 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (b ∈ (C ∩ B) ↔ (b ∈ C ⋀ b ∈ B))
53		elequ2 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (c = b → (x ∈ c ↔ x ∈ b))
54	53	biimprd 154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (c = b → (x ∈ b → x ∈ c))
55		eleq1 1537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (b = c → (b ∈ (C ∩ B) ↔ c ∈ (C ∩ B)))
56		incom 2211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 ⊢ (C ∩ B) = (B ∩ C)
57	56	eleq2i 1541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 ⊢ (c ∈ (C ∩ B) ↔ c ∈ (B ∩ C))
58	55, 57	syl6bb 538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (b = c → (b ∈ (C ∩ B) ↔ c ∈ (B ∩ C)))
59	58	equcoms 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (c = b → (b ∈ (C ∩ B) ↔ c ∈ (B ∩ C)))
60	59	biimpd 153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (c = b → (b ∈ (C ∩ B) → c ∈ (B ∩ C)))
61	54, 60	anim12d 560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (c = b → ((x ∈ b ⋀ b ∈ (C ∩ B)) → (x ∈ c ⋀ c ∈ (B ∩ C))))
62	61	a4imev 1275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((x ∈ b ⋀ b ∈ (C ∩ B)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))
63	62	expcom 374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (b ∈ (C ∩ B) → (x ∈ b → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))
64	52, 63	sylbir 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((b ∈ C ⋀ b ∈ B) → (x ∈ b → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))
65	64	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (b ∈ C → (b ∈ B → (x ∈ b → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))
66	51, 65	syl6bi 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (a = b → (a ∈ C → (b ∈ B → (x ∈ b → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
67	66	com3l 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (a ∈ C → (b ∈ B → (a = b → (x ∈ b → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
68	67	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((a ∈ C ⋀ b ∈ B) → (a = b → (x ∈ b → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))
69	68	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((a ∈ C ⋀ b ∈ B) → (x ∈ b → (a = b → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))
70	69	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((a ∈ C ⋀ b ∈ B) ⋀ x ∈ b) → (a = b → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))
71	50, 70	syl9 57	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((a ∈ C ⋀ (b ∈ B ⋀ x ∈ b)) ⋀ x ∈ a) ⋀ (a ∈ C → a ∈ (A / R))) → (((a ∈ C ⋀ b ∈ B) ⋀ x ∈ b) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))
72	71	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((a ∈ C ⋀ (b ∈ B ⋀ x ∈ b)) ⋀ x ∈ a) → ((a ∈ C → a ∈ (A / R)) → (((a ∈ C ⋀ b ∈ B) ⋀ x ∈ b) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
73	72	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((a ∈ C ⋀ (b ∈ B ⋀ x ∈ b)) ⋀ x ∈ a) → (((a ∈ C ⋀ b ∈ B) ⋀ x ∈ b) → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
74	73	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((a ∈ C ⋀ (b ∈ B ⋀ x ∈ b)) → (x ∈ a → (((a ∈ C ⋀ b ∈ B) ⋀ x ∈ b) → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))))
75	74	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((a ∈ C ⋀ (b ∈ B ⋀ x ∈ b)) → (((a ∈ C ⋀ b ∈ B) ⋀ x ∈ b) → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))))
76	75	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (a ∈ C → ((b ∈ B ⋀ x ∈ b) → (((a ∈ C ⋀ b ∈ B) ⋀ x ∈ b) → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))))
77	76	com3r 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((a ∈ C ⋀ b ∈ B) ⋀ x ∈ b) → (a ∈ C → ((b ∈ B ⋀ x ∈ b) → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))))
78	77	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((a ∈ C ⋀ b ∈ B) → (x ∈ b → (a ∈ C → ((b ∈ B ⋀ x ∈ b) → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))))))
79	78	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((a ∈ C ⋀ b ∈ B) → (a ∈ C → (x ∈ b → ((b ∈ B ⋀ x ∈ b) → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))))))
80	79	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (a ∈ C → (b ∈ B → (a ∈ C → (x ∈ b → ((b ∈ B ⋀ x ∈ b) → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))))))
81	80	pm2.43a 66	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (a ∈ C → (b ∈ B → (x ∈ b → ((b ∈ B ⋀ x ∈ b) → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))))))
82	81	com14 38	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((b ∈ B ⋀ x ∈ b) → (b ∈ B → (x ∈ b → (a ∈ C → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))))))
83	82	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (b ∈ B → (x ∈ b → (b ∈ B → (x ∈ b → (a ∈ C → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))))))
84	83	pm2.43a 66	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (b ∈ B → (x ∈ b → (x ∈ b → (a ∈ C → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))))))
85	84	com13 33	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (x ∈ b → (x ∈ b → (b ∈ B → (a ∈ C → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))))))
86	85	pm2.43i 64	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x ∈ b → (b ∈ B → (a ∈ C → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))))
87	86	imp 350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((x ∈ b ⋀ b ∈ B) → (a ∈ C → (x ∈ a → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))))
88	87	com13 33	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x ∈ a → (a ∈ C → ((x ∈ b ⋀ b ∈ B) → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))))
89	88	imp 350	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((x ∈ a ⋀ a ∈ C) → ((x ∈ b ⋀ b ∈ B) → ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
90	89	com4t 40	. . . . . . . . . . . . . . . . . . 19 ⊢ ((a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ((x ∈ a ⋀ a ∈ C) → ((x ∈ b ⋀ b ∈ B) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
91	90	a4s 986	. . . . . . . . . . . . . . . . . 18 ⊢ (∀a(a ∈ C → a ∈ (A / R)) → ((b ∈ B → b ∈ (A / R)) → ((x ∈ a ⋀ a ∈ C) → ((x ∈ b ⋀ b ∈ B) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
92	2, 91	sylbi 199	. . . . . . . . . . . . . . . . 17 ⊢ (C ⊆ (A / R) → ((b ∈ B → b ∈ (A / R)) → ((x ∈ a ⋀ a ∈ C) → ((x ∈ b ⋀ b ∈ B) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
93	92	com12 11	. . . . . . . . . . . . . . . 16 ⊢ ((b ∈ B → b ∈ (A / R)) → (C ⊆ (A / R) → ((x ∈ a ⋀ a ∈ C) → ((x ∈ b ⋀ b ∈ B) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
94	93	a4s 986	. . . . . . . . . . . . . . 15 ⊢ (∀b(b ∈ B → b ∈ (A / R)) → (C ⊆ (A / R) → ((x ∈ a ⋀ a ∈ C) → ((x ∈ b ⋀ b ∈ B) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
95	1, 94	sylbi 199	. . . . . . . . . . . . . 14 ⊢ (B ⊆ (A / R) → (C ⊆ (A / R) → ((x ∈ a ⋀ a ∈ C) → ((x ∈ b ⋀ b ∈ B) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C))))))
96	95	imp 350	. . . . . . . . . . . . 13 ⊢ ((B ⊆ (A / R) ⋀ C ⊆ (A / R)) → ((x ∈ a ⋀ a ∈ C) → ((x ∈ b ⋀ b ∈ B) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))
97	96	com12 11	. . . . . . . . . . . 12 ⊢ ((x ∈ a ⋀ a ∈ C) → ((B ⊆ (A / R) ⋀ C ⊆ (A / R)) → ((x ∈ b ⋀ b ∈ B) → ∃c(x ∈ c ⋀ c ∈ (B ∩ C)))))
98	97	19.23aiv 1297	. . . . . . . . . . 11 ⊢ (∃a(x ∈ a ⋀ a ∈ C) → ((B ⊆ (A / R) ⋀ C ⊆ (A / R)) → ((x