Theorem ecopovtrn 6139

Description: Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation ∼, specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)

Hypotheses

Ref	Expression
ecopopr.1	⊢ ∼ = {⟨x, y⟩ ∣ ((x ∈ (𝑆 × 𝑆) ∧ y ∈ (𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z + u) = (w + v)))}
ecopopr.com	⊢ (x + y) = (y + x)
ecopopr.cl	⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → (x + y) ∈ 𝑆)
ecopopr.ass	⊢ ((x + y) + z) = (x + (y + z))
ecopopr.can	⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → ((x + y) = (x + z) → y = z))

Assertion

Ref	Expression
ecopovtrn	⊢ ((A ∼ B ∧ B ∼ 𝐶) → A ∼ 𝐶)

Distinct variable groups:   x,y,z,w,v,u, +   x,𝑆,y,z,w,v,u

Allowed substitution hints:   A(x,y,z,w,v,u)   B(x,y,z,w,v,u)   𝐶(x,y,z,w,v,u)   ∼ (x,y,z,w,v,u)

Proof of Theorem ecopovtrn

Dummy variables f g ℎ 𝑡 𝑠 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ecopopr.1	. . . . . . 7 ⊢ ∼ = {⟨x, y⟩ ∣ ((x ∈ (𝑆 × 𝑆) ∧ y ∈ (𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z + u) = (w + v)))}
2		opabssxp 4357	. . . . . . 7 ⊢ {⟨x, y⟩ ∣ ((x ∈ (𝑆 × 𝑆) ∧ y ∈ (𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z + u) = (w + v)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
3	1, 2	eqsstri 2969	. . . . . 6 ⊢ ∼ ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
4	3	brel 4335	. . . . 5 ⊢ (A ∼ B → (A ∈ (𝑆 × 𝑆) ∧ B ∈ (𝑆 × 𝑆)))
5	4	simpld 105	. . . 4 ⊢ (A ∼ B → A ∈ (𝑆 × 𝑆))
6	3	brel 4335	. . . 4 ⊢ (B ∼ 𝐶 → (B ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
7	5, 6	anim12i 321	. . 3 ⊢ ((A ∼ B ∧ B ∼ 𝐶) → (A ∈ (𝑆 × 𝑆) ∧ (B ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
8		3anass 888	. . 3 ⊢ ((A ∈ (𝑆 × 𝑆) ∧ B ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) ↔ (A ∈ (𝑆 × 𝑆) ∧ (B ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
9	7, 8	sylibr 137	. 2 ⊢ ((A ∼ B ∧ B ∼ 𝐶) → (A ∈ (𝑆 × 𝑆) ∧ B ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
10		eqid 2037	. . 3 ⊢ (𝑆 × 𝑆) = (𝑆 × 𝑆)
11		breq1 3758	. . . . 5 ⊢ (⟨f, g⟩ = A → (⟨f, g⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ A ∼ ⟨ℎ, 𝑡⟩))
12	11	anbi1d 438	. . . 4 ⊢ (⟨f, g⟩ = A → ((⟨f, g⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ (A ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩)))
13		breq1 3758	. . . 4 ⊢ (⟨f, g⟩ = A → (⟨f, g⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ A ∼ ⟨𝑠, 𝑟⟩))
14	12, 13	imbi12d 223	. . 3 ⊢ (⟨f, g⟩ = A → (((⟨f, g⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ⟨f, g⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ ((A ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → A ∼ ⟨𝑠, 𝑟⟩)))
15		breq2 3759	. . . . 5 ⊢ (⟨ℎ, 𝑡⟩ = B → (A ∼ ⟨ℎ, 𝑡⟩ ↔ A ∼ B))
16		breq1 3758	. . . . 5 ⊢ (⟨ℎ, 𝑡⟩ = B → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ B ∼ ⟨𝑠, 𝑟⟩))
17	15, 16	anbi12d 442	. . . 4 ⊢ (⟨ℎ, 𝑡⟩ = B → ((A ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ (A ∼ B ∧ B ∼ ⟨𝑠, 𝑟⟩)))
18	17	imbi1d 220	. . 3 ⊢ (⟨ℎ, 𝑡⟩ = B → (((A ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → A ∼ ⟨𝑠, 𝑟⟩) ↔ ((A ∼ B ∧ B ∼ ⟨𝑠, 𝑟⟩) → A ∼ ⟨𝑠, 𝑟⟩)))
19		breq2 3759	. . . . 5 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (B ∼ ⟨𝑠, 𝑟⟩ ↔ B ∼ 𝐶))
20	19	anbi2d 437	. . . 4 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → ((A ∼ B ∧ B ∼ ⟨𝑠, 𝑟⟩) ↔ (A ∼ B ∧ B ∼ 𝐶)))
21		breq2 3759	. . . 4 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (A ∼ ⟨𝑠, 𝑟⟩ ↔ A ∼ 𝐶))
22	20, 21	imbi12d 223	. . 3 ⊢ (⟨𝑠, 𝑟⟩ = 𝐶 → (((A ∼ B ∧ B ∼ ⟨𝑠, 𝑟⟩) → A ∼ ⟨𝑠, 𝑟⟩) ↔ ((A ∼ B ∧ B ∼ 𝐶) → A ∼ 𝐶)))
23	1	ecopoveq 6137	. . . . . . . 8 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆)) → (⟨f, g⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ (f + 𝑡) = (g + ℎ)))
24	23	3adant3 923	. . . . . . 7 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨f, g⟩ ∼ ⟨ℎ, 𝑡⟩ ↔ (f + 𝑡) = (g + ℎ)))
25	1	ecopoveq 6137	. . . . . . . 8 ⊢ (((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (ℎ + 𝑟) = (𝑡 + 𝑠)))
26	25	3adant1 921	. . . . . . 7 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (ℎ + 𝑟) = (𝑡 + 𝑠)))
27	24, 26	anbi12d 442	. . . . . 6 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨f, g⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) ↔ ((f + 𝑡) = (g + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠))))
28		oveq12 5464	. . . . . . 7 ⊢ (((f + 𝑡) = (g + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)) → ((f + 𝑡) + (ℎ + 𝑟)) = ((g + ℎ) + (𝑡 + 𝑠)))
29		simp2l 929	. . . . . . . . 9 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ℎ ∈ 𝑆)
30		simp2r 930	. . . . . . . . 9 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → 𝑡 ∈ 𝑆)
31		simp1l 927	. . . . . . . . 9 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → f ∈ 𝑆)
32		ecopopr.com	. . . . . . . . . 10 ⊢ (x + y) = (y + x)
33	32	a1i 9	. . . . . . . . 9 ⊢ ((((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) = (y + x))
34		ecopopr.ass	. . . . . . . . . 10 ⊢ ((x + y) + z) = (x + (y + z))
35	34	a1i 9	. . . . . . . . 9 ⊢ ((((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x + y) + z) = (x + (y + z)))
36		simp3r 932	. . . . . . . . 9 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → 𝑟 ∈ 𝑆)
37		ecopopr.cl	. . . . . . . . . 10 ⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → (x + y) ∈ 𝑆)
38	37	adantl 262	. . . . . . . . 9 ⊢ ((((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x + y) ∈ 𝑆)
39	29, 30, 31, 33, 35, 36, 38	caov411d 5628	. . . . . . . 8 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((ℎ + 𝑡) + (f + 𝑟)) = ((f + 𝑡) + (ℎ + 𝑟)))
40		simp1r 928	. . . . . . . . . 10 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → g ∈ 𝑆)
41		simp3l 931	. . . . . . . . . 10 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → 𝑠 ∈ 𝑆)
42	40, 30, 29, 33, 35, 41, 38	caov411d 5628	. . . . . . . . 9 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((g + 𝑡) + (ℎ + 𝑠)) = ((ℎ + 𝑡) + (g + 𝑠)))
43	40, 30, 29, 33, 35, 41, 38	caov4d 5627	. . . . . . . . 9 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((g + 𝑡) + (ℎ + 𝑠)) = ((g + ℎ) + (𝑡 + 𝑠)))
44	42, 43	eqtr3d 2071	. . . . . . . 8 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((ℎ + 𝑡) + (g + 𝑠)) = ((g + ℎ) + (𝑡 + 𝑠)))
45	39, 44	eqeq12d 2051	. . . . . . 7 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (f + 𝑟)) = ((ℎ + 𝑡) + (g + 𝑠)) ↔ ((f + 𝑡) + (ℎ + 𝑟)) = ((g + ℎ) + (𝑡 + 𝑠))))
46	28, 45	syl5ibr 145	. . . . . 6 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((f + 𝑡) = (g + ℎ) ∧ (ℎ + 𝑟) = (𝑡 + 𝑠)) → ((ℎ + 𝑡) + (f + 𝑟)) = ((ℎ + 𝑡) + (g + 𝑠))))
47	27, 46	sylbid 139	. . . . 5 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨f, g⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ((ℎ + 𝑡) + (f + 𝑟)) = ((ℎ + 𝑡) + (g + 𝑠))))
48		ecopopr.can	. . . . . . . . 9 ⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆) → ((x + y) = (x + z) → y = z))
49	48	3adant3 923	. . . . . . . 8 ⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆) → ((x + y) = (x + z) → y = z))
50		oveq2 5463	. . . . . . . 8 ⊢ (y = z → (x + y) = (x + z))
51	49, 50	impbid1 130	. . . . . . 7 ⊢ ((x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆) → ((x + y) = (x + z) ↔ y = z))
52	51	adantl 262	. . . . . 6 ⊢ ((((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x + y) = (x + z) ↔ y = z))
53	37	caovcl 5597	. . . . . . 7 ⊢ ((ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) → (ℎ + 𝑡) ∈ 𝑆)
54	29, 30, 53	syl2anc 391	. . . . . 6 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (ℎ + 𝑡) ∈ 𝑆)
55	37	caovcl 5597	. . . . . . 7 ⊢ ((f ∈ 𝑆 ∧ 𝑟 ∈ 𝑆) → (f + 𝑟) ∈ 𝑆)
56	31, 36, 55	syl2anc 391	. . . . . 6 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (f + 𝑟) ∈ 𝑆)
57	38, 40, 41	caovcld 5596	. . . . . 6 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (g + 𝑠) ∈ 𝑆)
58	52, 54, 56, 57	caovcand 5605	. . . . 5 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (((ℎ + 𝑡) + (f + 𝑟)) = ((ℎ + 𝑡) + (g + 𝑠)) ↔ (f + 𝑟) = (g + 𝑠)))
59	47, 58	sylibd 138	. . . 4 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨f, g⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → (f + 𝑟) = (g + 𝑠)))
60	1	ecopoveq 6137	. . . . 5 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨f, g⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (f + 𝑟) = (g + 𝑠)))
61	60	3adant2 922	. . . 4 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → (⟨f, g⟩ ∼ ⟨𝑠, 𝑟⟩ ↔ (f + 𝑟) = (g + 𝑠)))
62	59, 61	sylibrd 158	. . 3 ⊢ (((f ∈ 𝑆 ∧ g ∈ 𝑆) ∧ (ℎ ∈ 𝑆 ∧ 𝑡 ∈ 𝑆) ∧ (𝑠 ∈ 𝑆 ∧ 𝑟 ∈ 𝑆)) → ((⟨f, g⟩ ∼ ⟨ℎ, 𝑡⟩ ∧ ⟨ℎ, 𝑡⟩ ∼ ⟨𝑠, 𝑟⟩) → ⟨f, g⟩ ∼ ⟨𝑠, 𝑟⟩))
63	10, 14, 18, 22, 62	3optocl 4361	. 2 ⊢ ((A ∈ (𝑆 × 𝑆) ∧ B ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) → ((A ∼ B ∧ B ∼ 𝐶) → A ∼ 𝐶))
64	9, 63	mpcom 32	1 ⊢ ((A ∼ B ∧ B ∼ 𝐶) → A ∼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755  {copab 3808   × cxp 4286  (class class class)co 5455

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-xp 4294  df-iota 4810  df-fv 4853  df-ov 5458

This theorem is referenced by:  ecopover  6140