Theorem genpass 3906

Description: Associativity of an operation on reals.

Hypotheses

Ref	Expression
genp.1	⊢ F = {⟨⟨w, v⟩, u⟩∣((w ∈ P ∧ v ∈ P) ∧ u = {x∣∃y ∈ w ∃z ∈ v x = (yGz)})}
genpass.2	⊢ B ∈ V
genpass.3	⊢ C ∈ V
genpass.4	⊢ dom F = (P × P)
genpass.5	⊢ ((f ∈ P ∧ g ∈ P) → (fFg) ∈ P)
genpass.6	⊢ ((fGg)Gh) = (fG(gGh))

Assertion

Ref	Expression
genpass	⊢ ((AFB)FC) = (AF(BFC))

Distinct variable group(s):   x,y,z,f,g,h,A   x,B,y,z,f,g,h   x,w,v,u,G,y,z,f,g,h   f,F,g   x,C,y,z,f,g,h   x,F,y,z,h

Proof of Theorem genpass

Step	Hyp	Ref	Expression
1		genp.1	. . . . . . . . 9 ⊢ F = {⟨⟨w, v⟩, u⟩∣((w ∈ P ∧ v ∈ P) ∧ u = {x∣∃y ∈ w ∃z ∈ v x = (yGz)})}
2		visset 1350	. . . . . . . . 9 ⊢ x ∈ V
3	1, 2	genpelv 3897	. . . . . . . 8 ⊢ (((AFB) ∈ P ∧ C ∈ P) → (x ∈ ((AFB)FC) ↔ ∃t∃h((t ∈ (AFB) ∧ h ∈ C) ∧ x = (tGh))))
4		genpass.5	. . . . . . . . 9 ⊢ ((f ∈ P ∧ g ∈ P) → (fFg) ∈ P)
5	4	caoprcl 3066	. . . . . . . 8 ⊢ ((A ∈ P ∧ B ∈ P) → (AFB) ∈ P)
6	3, 5	sylan 343	. . . . . . 7 ⊢ (((A ∈ P ∧ B ∈ P) ∧ C ∈ P) → (x ∈ ((AFB)FC) ↔ ∃t∃h((t ∈ (AFB) ∧ h ∈ C) ∧ x = (tGh))))
7	6	3impa 609	. . . . . 6 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (x ∈ ((AFB)FC) ↔ ∃t∃h((t ∈ (AFB) ∧ h ∈ C) ∧ x = (tGh))))
8		visset 1350	. . . . . . . . . . 11 ⊢ t ∈ V
9	1, 8	genpelv 3897	. . . . . . . . . 10 ⊢ ((A ∈ P ∧ B ∈ P) → (t ∈ (AFB) ↔ ∃f∃g((f ∈ A ∧ g ∈ B) ∧ t = (fGg))))
10	9	3adant3 599	. . . . . . . . 9 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (t ∈ (AFB) ↔ ∃f∃g((f ∈ A ∧ g ∈ B) ∧ t = (fGg))))
11	10	anbi1d 469	. . . . . . . 8 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → ((t ∈ (AFB) ∧ (h ∈ C ∧ x = (tGh))) ↔ (∃f∃g((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh)))))
12		anass 336	. . . . . . . 8 ⊢ (((t ∈ (AFB) ∧ h ∈ C) ∧ x = (tGh)) ↔ (t ∈ (AFB) ∧ (h ∈ C ∧ x = (tGh))))
13		19.41vv 964	. . . . . . . 8 ⊢ (∃f∃g(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ (∃f∃g((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))))
14	11, 12, 13	3bitr4g 428	. . . . . . 7 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (((t ∈ (AFB) ∧ h ∈ C) ∧ x = (tGh)) ↔ ∃f∃g(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh)))))
15	14	bi2exdv 938	. . . . . 6 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (∃t∃h((t ∈ (AFB) ∧ h ∈ C) ∧ x = (tGh)) ↔ ∃t∃h∃f∃g(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh)))))
16	7, 15	bitrd 406	. . . . 5 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (x ∈ ((AFB)FC) ↔ ∃t∃h∃f∃g(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh)))))
17		exrot4 778	. . . . . 6 ⊢ (∃t∃h∃f∃g(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ ∃f∃g∃t∃h(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))))
18		excom 728	. . . . . . . 8 ⊢ (∃t∃h(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ ∃h∃t(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))))
19		an4 388	. . . . . . . . . . . 12 ⊢ ((((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ (((f ∈ A ∧ g ∈ B) ∧ h ∈ C) ∧ (t = (fGg) ∧ x = (tGh))))
20		anass 336	. . . . . . . . . . . . 13 ⊢ (((f ∈ A ∧ g ∈ B) ∧ h ∈ C) ↔ (f ∈ A ∧ (g ∈ B ∧ h ∈ C)))
21		opreq1 3006	. . . . . . . . . . . . . . . 16 ⊢ (t = (fGg) → (tGh) = ((fGg)Gh))
22		genpass.6	. . . . . . . . . . . . . . . 16 ⊢ ((fGg)Gh) = (fG(gGh))
23	21, 22	syl6eq 1140	. . . . . . . . . . . . . . 15 ⊢ (t = (fGg) → (tGh) = (fG(gGh)))
24	23	cleq2d 1112	. . . . . . . . . . . . . 14 ⊢ (t = (fGg) → (x = (tGh) ↔ x = (fG(gGh))))
25	24	pm5.32i 489	. . . . . . . . . . . . 13 ⊢ ((t = (fGg) ∧ x = (tGh)) ↔ (t = (fGg) ∧ x = (fG(gGh))))
26	20, 25	anbi12i 369	. . . . . . . . . . . 12 ⊢ ((((f ∈ A ∧ g ∈ B) ∧ h ∈ C) ∧ (t = (fGg) ∧ x = (tGh))) ↔ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ (t = (fGg) ∧ x = (fG(gGh)))))
27		an12 370	. . . . . . . . . . . 12 ⊢ (((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ (t = (fGg) ∧ x = (fG(gGh)))) ↔ (t = (fGg) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
28	19, 26, 27	3bitr 155	. . . . . . . . . . 11 ⊢ ((((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ (t = (fGg) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
29	28	biex 733	. . . . . . . . . 10 ⊢ (∃t(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ ∃t(t = (fGg) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
30		19.41v 963	. . . . . . . . . . 11 ⊢ (∃t(t = (fGg) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))) ↔ (∃t t = (fGg) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
31		oprex 3018	. . . . . . . . . . . 12 ⊢ (fGg) ∈ V
32	31	isseti 1352	. . . . . . . . . . 11 ⊢ ∃t t = (fGg)
33	30, 32	mpbiran 547	. . . . . . . . . 10 ⊢ (∃t(t = (fGg) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))) ↔ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
34	29, 33	bitr 151	. . . . . . . . 9 ⊢ (∃t(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
35	34	biex 733	. . . . . . . 8 ⊢ (∃h∃t(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ ∃h((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
36	18, 35	bitr 151	. . . . . . 7 ⊢ (∃t∃h(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ ∃h((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
37	36	bi2ex 734	. . . . . 6 ⊢ (∃f∃g∃t∃h(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ ∃f∃g∃h((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
38	17, 37	bitr 151	. . . . 5 ⊢ (∃t∃h∃f∃g(((f ∈ A ∧ g ∈ B) ∧ t = (fGg)) ∧ (h ∈ C ∧ x = (tGh))) ↔ ∃f∃g∃h((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
39	16, 38	syl6bb 414	. . . 4 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (x ∈ ((AFB)FC) ↔ ∃f∃g∃h((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
40	1, 2	genpelv 3897	. . . . . . 7 ⊢ ((A ∈ P ∧ (BFC) ∈ P) → (x ∈ (AF(BFC)) ↔ ∃f∃t((f ∈ A ∧ t ∈ (BFC)) ∧ x = (fGt))))
41	4	caoprcl 3066	. . . . . . 7 ⊢ ((B ∈ P ∧ C ∈ P) → (BFC) ∈ P)
42	40, 41	sylan2 346	. . . . . 6 ⊢ ((A ∈ P ∧ (B ∈ P ∧ C ∈ P)) → (x ∈ (AF(BFC)) ↔ ∃f∃t((f ∈ A ∧ t ∈ (BFC)) ∧ x = (fGt))))
43	42	3impb 610	. . . . 5 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (x ∈ (AF(BFC)) ↔ ∃f∃t((f ∈ A ∧ t ∈ (BFC)) ∧ x = (fGt))))
44	1, 8	genpelv 3897	. . . . . . . . . 10 ⊢ ((B ∈ P ∧ C ∈ P) → (t ∈ (BFC) ↔ ∃g∃h((g ∈ B ∧ h ∈ C) ∧ t = (gGh))))
45	44	3adant1 597	. . . . . . . . 9 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (t ∈ (BFC) ↔ ∃g∃h((g ∈ B ∧ h ∈ C) ∧ t = (gGh))))
46	45	anbi1d 469	. . . . . . . 8 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → ((t ∈ (BFC) ∧ (f ∈ A ∧ x = (fGt))) ↔ (∃g∃h((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt)))))
47		anass 336	. . . . . . . . 9 ⊢ (((f ∈ A ∧ t ∈ (BFC)) ∧ x = (fGt)) ↔ (f ∈ A ∧ (t ∈ (BFC) ∧ x = (fGt))))
48		an12 370	. . . . . . . . 9 ⊢ ((f ∈ A ∧ (t ∈ (BFC) ∧ x = (fGt))) ↔ (t ∈ (BFC) ∧ (f ∈ A ∧ x = (fGt))))
49	47, 48	bitr 151	. . . . . . . 8 ⊢ (((f ∈ A ∧ t ∈ (BFC)) ∧ x = (fGt)) ↔ (t ∈ (BFC) ∧ (f ∈ A ∧ x = (fGt))))
50		19.41vv 964	. . . . . . . 8 ⊢ (∃g∃h(((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))) ↔ (∃g∃h((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))))
51	46, 49, 50	3bitr4g 428	. . . . . . 7 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (((f ∈ A ∧ t ∈ (BFC)) ∧ x = (fGt)) ↔ ∃g∃h(((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt)))))
52	51	bi2exdv 938	. . . . . 6 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (∃f∃t((f ∈ A ∧ t ∈ (BFC)) ∧ x = (fGt)) ↔ ∃f∃t∃g∃h(((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt)))))
53		exrot3 777	. . . . . . . 8 ⊢ (∃t∃g∃h(((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))) ↔ ∃g∃h∃t(((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))))
54		an4 388	. . . . . . . . . . . 12 ⊢ ((((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))) ↔ (((g ∈ B ∧ h ∈ C) ∧ f ∈ A) ∧ (t = (gGh) ∧ x = (fGt))))
55		ancom 333	. . . . . . . . . . . . 13 ⊢ (((g ∈ B ∧ h ∈ C) ∧ f ∈ A) ↔ (f ∈ A ∧ (g ∈ B ∧ h ∈ C)))
56		opreq2 3007	. . . . . . . . . . . . . . 15 ⊢ (t = (gGh) → (fGt) = (fG(gGh)))
57	56	cleq2d 1112	. . . . . . . . . . . . . 14 ⊢ (t = (gGh) → (x = (fGt) ↔ x = (fG(gGh))))
58	57	pm5.32i 489	. . . . . . . . . . . . 13 ⊢ ((t = (gGh) ∧ x = (fGt)) ↔ (t = (gGh) ∧ x = (fG(gGh))))
59	55, 58	anbi12i 369	. . . . . . . . . . . 12 ⊢ ((((g ∈ B ∧ h ∈ C) ∧ f ∈ A) ∧ (t = (gGh) ∧ x = (fGt))) ↔ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ (t = (gGh) ∧ x = (fG(gGh)))))
60		an12 370	. . . . . . . . . . . 12 ⊢ (((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ (t = (gGh) ∧ x = (fG(gGh)))) ↔ (t = (gGh) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
61	54, 59, 60	3bitr 155	. . . . . . . . . . 11 ⊢ ((((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))) ↔ (t = (gGh) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
62	61	biex 733	. . . . . . . . . 10 ⊢ (∃t(((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))) ↔ ∃t(t = (gGh) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
63		19.41v 963	. . . . . . . . . . 11 ⊢ (∃t(t = (gGh) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))) ↔ (∃t t = (gGh) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
64		oprex 3018	. . . . . . . . . . . 12 ⊢ (gGh) ∈ V
65	64	isseti 1352	. . . . . . . . . . 11 ⊢ ∃t t = (gGh)
66	63, 65	mpbiran 547	. . . . . . . . . 10 ⊢ (∃t(t = (gGh) ∧ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))) ↔ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
67	62, 66	bitr 151	. . . . . . . . 9 ⊢ (∃t(((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))) ↔ ((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
68	67	bi2ex 734	. . . . . . . 8 ⊢ (∃g∃h∃t(((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))) ↔ ∃g∃h((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
69	53, 68	bitr 151	. . . . . . 7 ⊢ (∃t∃g∃h(((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))) ↔ ∃g∃h((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
70	69	biex 733	. . . . . 6 ⊢ (∃f∃t∃g∃h(((g ∈ B ∧ h ∈ C) ∧ t = (gGh)) ∧ (f ∈ A ∧ x = (fGt))) ↔ ∃f∃g∃h((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh))))
71	52, 70	syl6bb 414	. . . . 5 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (∃f∃t((f ∈ A ∧ t ∈ (BFC)) ∧ x = (fGt)) ↔ ∃f∃g∃h((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
72	43, 71	bitrd 406	. . . 4 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (x ∈ (AF(BFC)) ↔ ∃f∃g∃h((f ∈ A ∧ (g ∈ B ∧ h ∈ C)) ∧ x = (fG(gGh)))))
73	39, 72	bitr4d 409	. . 3 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → (x ∈ ((AFB)FC) ↔ x ∈ (AF(BFC))))
74	73	cleqrd 1100	. 2 ⊢ ((A ∈ P ∧ B ∈ P ∧ C ∈ P) → ((AFB)FC) = (AF(BFC)))
75		genpass.2	. . 3 ⊢ B ∈ V
76		genpass.4	. . 3 ⊢ dom F = (P × P)
77		genpass.3	. . 3 ⊢ C ∈ V
78		0npr 3890	. . 3 ⊢ ¬ ∅ ∈ P
79	75, 76, 77, 78	ndmoprass 3062	. 2 ⊢ (¬ (A ∈ P ∧ B ∈ P ∧ C ∈ P) → ((AFB)FC) = (AF(BFC)))
80	74, 79	pm2.61i 110	1 ⊢ ((AFB)FC) = (AF(BFC))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   ∧ w3a 581  ∃wex 678  {cab 1090   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  Vcvv 1348   × cxp 2408  dom cdm 2410  (class class class)co 3001  {copab2 3002  Pcnp 3779

This theorem is referenced by:  addasspr 3918  mulasspr 3920

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-qs 3205  df-ni 3794  df-nq 3832  df-np 3880

metamath.org