Theorem genpassu 6508

Description: Associativity of upper cuts. Lemma for genpassg 6509. (Contributed by Jim Kingdon, 11-Dec-2019.)

Hypotheses

Ref	Expression
genpelvl.1	⊢ 𝐹 = (w ∈ P, v ∈ P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1st ‘w) ∧ z ∈ (1st ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2nd ‘w) ∧ z ∈ (2nd ‘v) ∧ x = (y𝐺z))}⟩)
genpelvl.2	⊢ ((y ∈ Q ∧ z ∈ Q) → (y𝐺z) ∈ Q)
genpassg.4	⊢ dom 𝐹 = (P × P)
genpassg.5	⊢ ((f ∈ P ∧ g ∈ P) → (f𝐹g) ∈ P)
genpassg.6	⊢ ((f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q) → ((f𝐺g)𝐺ℎ) = (f𝐺(g𝐺ℎ)))

Assertion

Ref	Expression
genpassu	⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (2nd ‘((A𝐹B)𝐹𝐶)) = (2nd ‘(A𝐹(B𝐹𝐶))))

Distinct variable groups:   x,y,z,f,g,ℎ,w,v,A   x,B,y,z,f,g,ℎ,w,v   x,𝐺,y,z,f,g,ℎ,w,v   f,𝐹,g   𝐶,f,g,ℎ,v,w,x,y,z   ℎ,𝐹,v,w,x,y,z

Proof of Theorem genpassu

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		prop 6458	. . . . . . . . 9 ⊢ (A ∈ P → ⟨(1st ‘A), (2nd ‘A)⟩ ∈ P)
2		elprnqu 6465	. . . . . . . . 9 ⊢ ((⟨(1st ‘A), (2nd ‘A)⟩ ∈ P ∧ f ∈ (2nd ‘A)) → f ∈ Q)
3	1, 2	sylan 267	. . . . . . . 8 ⊢ ((A ∈ P ∧ f ∈ (2nd ‘A)) → f ∈ Q)
4		prop 6458	. . . . . . . . . . . . . . . 16 ⊢ (B ∈ P → ⟨(1st ‘B), (2nd ‘B)⟩ ∈ P)
5		elprnqu 6465	. . . . . . . . . . . . . . . 16 ⊢ ((⟨(1st ‘B), (2nd ‘B)⟩ ∈ P ∧ g ∈ (2nd ‘B)) → g ∈ Q)
6	4, 5	sylan 267	. . . . . . . . . . . . . . 15 ⊢ ((B ∈ P ∧ g ∈ (2nd ‘B)) → g ∈ Q)
7		r19.41v 2460	. . . . . . . . . . . . . . . . 17 ⊢ (∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))
8		prop 6458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 ∈ P → ⟨(1st ‘𝐶), (2nd ‘𝐶)⟩ ∈ P)
9		elprnqu 6465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨(1st ‘𝐶), (2nd ‘𝐶)⟩ ∈ P ∧ ℎ ∈ (2nd ‘𝐶)) → ℎ ∈ Q)
10	8, 9	sylan 267	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ P ∧ ℎ ∈ (2nd ‘𝐶)) → ℎ ∈ Q)
11		oveq2 5463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = (g𝐺ℎ) → (f𝐺𝑡) = (f𝐺(g𝐺ℎ)))
12	11	adantr 261	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = (g𝐺ℎ) ∧ (f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q)) → (f𝐺𝑡) = (f𝐺(g𝐺ℎ)))
13		genpassg.6	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q) → ((f𝐺g)𝐺ℎ) = (f𝐺(g𝐺ℎ)))
14	13	adantl 262	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = (g𝐺ℎ) ∧ (f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q)) → ((f𝐺g)𝐺ℎ) = (f𝐺(g𝐺ℎ)))
15	12, 14	eqtr4d 2072	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = (g𝐺ℎ) ∧ (f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q)) → (f𝐺𝑡) = ((f𝐺g)𝐺ℎ))
16	15	eqeq2d 2048	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = (g𝐺ℎ) ∧ (f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q)) → (x = (f𝐺𝑡) ↔ x = ((f𝐺g)𝐺ℎ)))
17	16	expcom 109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q) → (𝑡 = (g𝐺ℎ) → (x = (f𝐺𝑡) ↔ x = ((f𝐺g)𝐺ℎ))))
18	17	pm5.32d 423	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((f ∈ Q ∧ g ∈ Q ∧ ℎ ∈ Q) → ((𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
19	18	3expa 1103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((f ∈ Q ∧ g ∈ Q) ∧ ℎ ∈ Q) → ((𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
20	10, 19	sylan2 270	. . . . . . . . . . . . . . . . . . 19 ⊢ (((f ∈ Q ∧ g ∈ Q) ∧ (𝐶 ∈ P ∧ ℎ ∈ (2nd ‘𝐶))) → ((𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
21	20	anassrs 380	. . . . . . . . . . . . . . . . . 18 ⊢ ((((f ∈ Q ∧ g ∈ Q) ∧ 𝐶 ∈ P) ∧ ℎ ∈ (2nd ‘𝐶)) → ((𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
22	21	rexbidva 2317	. . . . . . . . . . . . . . . . 17 ⊢ (((f ∈ Q ∧ g ∈ Q) ∧ 𝐶 ∈ P) → (∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ ∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
23	7, 22	syl5rbbr 184	. . . . . . . . . . . . . . . 16 ⊢ (((f ∈ Q ∧ g ∈ Q) ∧ 𝐶 ∈ P) → (∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
24	23	an32s 502	. . . . . . . . . . . . . . 15 ⊢ (((f ∈ Q ∧ 𝐶 ∈ P) ∧ g ∈ Q) → (∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
25	6, 24	sylan2 270	. . . . . . . . . . . . . 14 ⊢ (((f ∈ Q ∧ 𝐶 ∈ P) ∧ (B ∈ P ∧ g ∈ (2nd ‘B))) → (∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
26	25	anassrs 380	. . . . . . . . . . . . 13 ⊢ ((((f ∈ Q ∧ 𝐶 ∈ P) ∧ B ∈ P) ∧ g ∈ (2nd ‘B)) → (∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
27	26	rexbidva 2317	. . . . . . . . . . . 12 ⊢ (((f ∈ Q ∧ 𝐶 ∈ P) ∧ B ∈ P) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ ∃g ∈ (2nd ‘B)(∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
28		r19.41v 2460	. . . . . . . . . . . 12 ⊢ (∃g ∈ (2nd ‘B)(∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)) ↔ (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡)))
29	27, 28	syl6bb 185	. . . . . . . . . . 11 ⊢ (((f ∈ Q ∧ 𝐶 ∈ P) ∧ B ∈ P) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
30	29	an31s 504	. . . . . . . . . 10 ⊢ (((B ∈ P ∧ 𝐶 ∈ P) ∧ f ∈ Q) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
31	30	exbidv 1703	. . . . . . . . 9 ⊢ (((B ∈ P ∧ 𝐶 ∈ P) ∧ f ∈ Q) → (∃𝑡∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ ∃𝑡(∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
32		genpelvl.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((y ∈ Q ∧ z ∈ Q) → (y𝐺z) ∈ Q)
33	32	caovcl 5597	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((g ∈ Q ∧ ℎ ∈ Q) → (g𝐺ℎ) ∈ Q)
34		elisset 2562	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((g𝐺ℎ) ∈ Q → ∃𝑡 𝑡 = (g𝐺ℎ))
35	33, 34	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((g ∈ Q ∧ ℎ ∈ Q) → ∃𝑡 𝑡 = (g𝐺ℎ))
36	35	biantrurd 289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((g ∈ Q ∧ ℎ ∈ Q) → (x = ((f𝐺g)𝐺ℎ) ↔ (∃𝑡 𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
37		19.41v 1779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ (∃𝑡 𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))
38	36, 37	syl6bbr 187	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((g ∈ Q ∧ ℎ ∈ Q) → (x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
39	10, 38	sylan2 270	. . . . . . . . . . . . . . . . . . 19 ⊢ ((g ∈ Q ∧ (𝐶 ∈ P ∧ ℎ ∈ (2nd ‘𝐶))) → (x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
40	39	anassrs 380	. . . . . . . . . . . . . . . . . 18 ⊢ (((g ∈ Q ∧ 𝐶 ∈ P) ∧ ℎ ∈ (2nd ‘𝐶)) → (x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
41	40	rexbidva 2317	. . . . . . . . . . . . . . . . 17 ⊢ ((g ∈ Q ∧ 𝐶 ∈ P) → (∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃ℎ ∈ (2nd ‘𝐶)∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
42		rexcom4 2571	. . . . . . . . . . . . . . . . 17 ⊢ (∃ℎ ∈ (2nd ‘𝐶)∃𝑡(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ ∃𝑡∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))
43	41, 42	syl6bb 185	. . . . . . . . . . . . . . . 16 ⊢ ((g ∈ Q ∧ 𝐶 ∈ P) → (∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
44	43	ancoms 255	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ P ∧ g ∈ Q) → (∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
45	6, 44	sylan2 270	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ P ∧ (B ∈ P ∧ g ∈ (2nd ‘B))) → (∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
46	45	anassrs 380	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ P ∧ B ∈ P) ∧ g ∈ (2nd ‘B)) → (∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
47	46	rexbidva 2317	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ P ∧ B ∈ P) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃g ∈ (2nd ‘B)∃𝑡∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
48	47	ancoms 255	. . . . . . . . . . 11 ⊢ ((B ∈ P ∧ 𝐶 ∈ P) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃g ∈ (2nd ‘B)∃𝑡∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
49		rexcom4 2571	. . . . . . . . . . 11 ⊢ (∃g ∈ (2nd ‘B)∃𝑡∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)) ↔ ∃𝑡∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ)))
50	48, 49	syl6bb 185	. . . . . . . . . 10 ⊢ ((B ∈ P ∧ 𝐶 ∈ P) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
51	50	adantr 261	. . . . . . . . 9 ⊢ (((B ∈ P ∧ 𝐶 ∈ P) ∧ f ∈ Q) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)(𝑡 = (g𝐺ℎ) ∧ x = ((f𝐺g)𝐺ℎ))))
52		df-rex 2306	. . . . . . . . . . 11 ⊢ (∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡) ↔ ∃𝑡(𝑡 ∈ (2nd ‘(B𝐹𝐶)) ∧ x = (f𝐺𝑡)))
53		genpelvl.1	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (w ∈ P, v ∈ P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1st ‘w) ∧ z ∈ (1st ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2nd ‘w) ∧ z ∈ (2nd ‘v) ∧ x = (y𝐺z))}⟩)
54	53, 32	genpelvu 6496	. . . . . . . . . . . . 13 ⊢ ((B ∈ P ∧ 𝐶 ∈ P) → (𝑡 ∈ (2nd ‘(B𝐹𝐶)) ↔ ∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ)))
55	54	anbi1d 438	. . . . . . . . . . . 12 ⊢ ((B ∈ P ∧ 𝐶 ∈ P) → ((𝑡 ∈ (2nd ‘(B𝐹𝐶)) ∧ x = (f𝐺𝑡)) ↔ (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
56	55	exbidv 1703	. . . . . . . . . . 11 ⊢ ((B ∈ P ∧ 𝐶 ∈ P) → (∃𝑡(𝑡 ∈ (2nd ‘(B𝐹𝐶)) ∧ x = (f𝐺𝑡)) ↔ ∃𝑡(∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
57	52, 56	syl5bb 181	. . . . . . . . . 10 ⊢ ((B ∈ P ∧ 𝐶 ∈ P) → (∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡) ↔ ∃𝑡(∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
58	57	adantr 261	. . . . . . . . 9 ⊢ (((B ∈ P ∧ 𝐶 ∈ P) ∧ f ∈ Q) → (∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡) ↔ ∃𝑡(∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)𝑡 = (g𝐺ℎ) ∧ x = (f𝐺𝑡))))
59	31, 51, 58	3bitr4rd 210	. . . . . . . 8 ⊢ (((B ∈ P ∧ 𝐶 ∈ P) ∧ f ∈ Q) → (∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡) ↔ ∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
60	3, 59	sylan2 270	. . . . . . 7 ⊢ (((B ∈ P ∧ 𝐶 ∈ P) ∧ (A ∈ P ∧ f ∈ (2nd ‘A))) → (∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡) ↔ ∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
61	60	anassrs 380	. . . . . 6 ⊢ ((((B ∈ P ∧ 𝐶 ∈ P) ∧ A ∈ P) ∧ f ∈ (2nd ‘A)) → (∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡) ↔ ∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
62	61	rexbidva 2317	. . . . 5 ⊢ (((B ∈ P ∧ 𝐶 ∈ P) ∧ A ∈ P) → (∃f ∈ (2nd ‘A)∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡) ↔ ∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
63	62	ancoms 255	. . . 4 ⊢ ((A ∈ P ∧ (B ∈ P ∧ 𝐶 ∈ P)) → (∃f ∈ (2nd ‘A)∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡) ↔ ∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
64	63	3impb 1099	. . 3 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (∃f ∈ (2nd ‘A)∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡) ↔ ∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
65		genpassg.5	. . . . . 6 ⊢ ((f ∈ P ∧ g ∈ P) → (f𝐹g) ∈ P)
66	65	caovcl 5597	. . . . 5 ⊢ ((B ∈ P ∧ 𝐶 ∈ P) → (B𝐹𝐶) ∈ P)
67	53, 32	genpelvu 6496	. . . . 5 ⊢ ((A ∈ P ∧ (B𝐹𝐶) ∈ P) → (x ∈ (2nd ‘(A𝐹(B𝐹𝐶))) ↔ ∃f ∈ (2nd ‘A)∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡)))
68	66, 67	sylan2 270	. . . 4 ⊢ ((A ∈ P ∧ (B ∈ P ∧ 𝐶 ∈ P)) → (x ∈ (2nd ‘(A𝐹(B𝐹𝐶))) ↔ ∃f ∈ (2nd ‘A)∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡)))
69	68	3impb 1099	. . 3 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (x ∈ (2nd ‘(A𝐹(B𝐹𝐶))) ↔ ∃f ∈ (2nd ‘A)∃𝑡 ∈ (2nd ‘(B𝐹𝐶))x = (f𝐺𝑡)))
70		df-rex 2306	. . . . 5 ⊢ (∃𝑡 ∈ (2nd ‘(A𝐹B))∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ) ↔ ∃𝑡(𝑡 ∈ (2nd ‘(A𝐹B)) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
71	53, 32	genpelvu 6496	. . . . . . . 8 ⊢ ((A ∈ P ∧ B ∈ P) → (𝑡 ∈ (2nd ‘(A𝐹B)) ↔ ∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g)))
72	71	3adant3 923	. . . . . . 7 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (𝑡 ∈ (2nd ‘(A𝐹B)) ↔ ∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g)))
73	72	anbi1d 438	. . . . . 6 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → ((𝑡 ∈ (2nd ‘(A𝐹B)) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ (∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
74	73	exbidv 1703	. . . . 5 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (∃𝑡(𝑡 ∈ (2nd ‘(A𝐹B)) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ ∃𝑡(∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
75	70, 74	syl5bb 181	. . . 4 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (∃𝑡 ∈ (2nd ‘(A𝐹B))∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ) ↔ ∃𝑡(∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
76	65	caovcl 5597	. . . . . 6 ⊢ ((A ∈ P ∧ B ∈ P) → (A𝐹B) ∈ P)
77	53, 32	genpelvu 6496	. . . . . 6 ⊢ (((A𝐹B) ∈ P ∧ 𝐶 ∈ P) → (x ∈ (2nd ‘((A𝐹B)𝐹𝐶)) ↔ ∃𝑡 ∈ (2nd ‘(A𝐹B))∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
78	76, 77	sylan 267	. . . . 5 ⊢ (((A ∈ P ∧ B ∈ P) ∧ 𝐶 ∈ P) → (x ∈ (2nd ‘((A𝐹B)𝐹𝐶)) ↔ ∃𝑡 ∈ (2nd ‘(A𝐹B))∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
79	78	3impa 1098	. . . 4 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (x ∈ (2nd ‘((A𝐹B)𝐹𝐶)) ↔ ∃𝑡 ∈ (2nd ‘(A𝐹B))∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
80	32	caovcl 5597	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f ∈ Q ∧ g ∈ Q) → (f𝐺g) ∈ Q)
81		elisset 2562	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f𝐺g) ∈ Q → ∃𝑡 𝑡 = (f𝐺g))
82	80, 81	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((f ∈ Q ∧ g ∈ Q) → ∃𝑡 𝑡 = (f𝐺g))
83	82	biantrurd 289	. . . . . . . . . . . . . . . . 17 ⊢ ((f ∈ Q ∧ g ∈ Q) → (∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ (∃𝑡 𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ))))
84		oveq1 5462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = (f𝐺g) → (𝑡𝐺ℎ) = ((f𝐺g)𝐺ℎ))
85	84	eqeq2d 2048	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = (f𝐺g) → (x = (𝑡𝐺ℎ) ↔ x = ((f𝐺g)𝐺ℎ)))
86	85	rexbidv 2321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = (f𝐺g) → (∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ) ↔ ∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
87	86	pm5.32i 427	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ (𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
88	87	exbii 1493	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ ∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
89		19.41v 1779	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)) ↔ (∃𝑡 𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
90	88, 89	bitri 173	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ (∃𝑡 𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
91	83, 90	syl6bbr 187	. . . . . . . . . . . . . . . 16 ⊢ ((f ∈ Q ∧ g ∈ Q) → (∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
92	6, 91	sylan2 270	. . . . . . . . . . . . . . 15 ⊢ ((f ∈ Q ∧ (B ∈ P ∧ g ∈ (2nd ‘B))) → (∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
93	92	anassrs 380	. . . . . . . . . . . . . 14 ⊢ (((f ∈ Q ∧ B ∈ P) ∧ g ∈ (2nd ‘B)) → (∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
94	93	rexbidva 2317	. . . . . . . . . . . . 13 ⊢ ((f ∈ Q ∧ B ∈ P) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃g ∈ (2nd ‘B)∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
95		rexcom4 2571	. . . . . . . . . . . . 13 ⊢ (∃g ∈ (2nd ‘B)∃𝑡(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ ∃𝑡∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
96	94, 95	syl6bb 185	. . . . . . . . . . . 12 ⊢ ((f ∈ Q ∧ B ∈ P) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
97	96	ancoms 255	. . . . . . . . . . 11 ⊢ ((B ∈ P ∧ f ∈ Q) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
98	3, 97	sylan2 270	. . . . . . . . . 10 ⊢ ((B ∈ P ∧ (A ∈ P ∧ f ∈ (2nd ‘A))) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
99	98	anassrs 380	. . . . . . . . 9 ⊢ (((B ∈ P ∧ A ∈ P) ∧ f ∈ (2nd ‘A)) → (∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
100	99	rexbidva 2317	. . . . . . . 8 ⊢ ((B ∈ P ∧ A ∈ P) → (∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃f ∈ (2nd ‘A)∃𝑡∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
101		rexcom4 2571	. . . . . . . 8 ⊢ (∃f ∈ (2nd ‘A)∃𝑡∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ ∃𝑡∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
102	100, 101	syl6bb 185	. . . . . . 7 ⊢ ((B ∈ P ∧ A ∈ P) → (∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
103		r19.41v 2460	. . . . . . . . . 10 ⊢ (∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ (∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
104	103	rexbii 2325	. . . . . . . . 9 ⊢ (∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ ∃f ∈ (2nd ‘A)(∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
105		r19.41v 2460	. . . . . . . . 9 ⊢ (∃f ∈ (2nd ‘A)(∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ (∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
106	104, 105	bitri 173	. . . . . . . 8 ⊢ (∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ (∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
107	106	exbii 1493	. . . . . . 7 ⊢ (∃𝑡∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)(𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)) ↔ ∃𝑡(∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ)))
108	102, 107	syl6bb 185	. . . . . 6 ⊢ ((B ∈ P ∧ A ∈ P) → (∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
109	108	ancoms 255	. . . . 5 ⊢ ((A ∈ P ∧ B ∈ P) → (∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
110	109	3adant3 923	. . . 4 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ) ↔ ∃𝑡(∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)𝑡 = (f𝐺g) ∧ ∃ℎ ∈ (2nd ‘𝐶)x = (𝑡𝐺ℎ))))
111	75, 79, 110	3bitr4d 209	. . 3 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (x ∈ (2nd ‘((A𝐹B)𝐹𝐶)) ↔ ∃f ∈ (2nd ‘A)∃g ∈ (2nd ‘B)∃ℎ ∈ (2nd ‘𝐶)x = ((f𝐺g)𝐺ℎ)))
112	64, 69, 111	3bitr4rd 210	. 2 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (x ∈ (2nd ‘((A𝐹B)𝐹𝐶)) ↔ x ∈ (2nd ‘(A𝐹(B𝐹𝐶)))))
113	112	eqrdv 2035	1 ⊢ ((A ∈ P ∧ B ∈ P ∧ 𝐶 ∈ P) → (2nd ‘((A𝐹B)𝐹𝐶)) = (2nd ‘(A𝐹(B𝐹𝐶))))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ∃wrex 2301  {crab 2304  ⟨cop 3370   × cxp 4286  dom cdm 4288  ‘cfv 4845  (class class class)co 5455   ↦ cmpt2 5457  1^st c1st 5707  2^nd c2nd 5708  Qcnq 6264  Pcnp 6275

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-in1 544  ax-in2 545  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-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  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-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  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-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-qs 6048  df-ni 6288  df-nqqs 6332  df-inp 6449

This theorem is referenced by:  genpassg  6509