genpassl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > genpassl		GIF version

Theorem genpassl 7233

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

**Hypotheses**
Ref	Expression
genpelvl.1	⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^st ‘𝑤) ∧ 𝑧 ∈ (1^st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^nd ‘𝑤) ∧ 𝑧 ∈ (2^nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)
genpelvl.2	⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)
genpassg.4	⊢ dom 𝐹 = (P × P)
genpassg.5	⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓𝐹𝑔) ∈ P)
genpassg.6	⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ)))

**Assertion**
Ref	Expression
genpassl	⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (1^st ‘((𝐴𝐹𝐵)𝐹𝐶)) = (1^st ‘(𝐴𝐹(𝐵𝐹𝐶))))

Distinct variable groups: 𝑥,𝑦,𝑧,𝑓,𝑔,ℎ,𝑤,𝑣,𝐴 𝑥,𝐵,𝑦,𝑧,𝑓,𝑔,ℎ,𝑤,𝑣 𝑥,𝐺,𝑦,𝑧,𝑓,𝑔,ℎ,𝑤,𝑣 𝑓,𝐹,𝑔 𝐶,𝑓,𝑔,ℎ,𝑣,𝑤,𝑥,𝑦,𝑧 ℎ,𝐹,𝑣,𝑤,𝑥,𝑦,𝑧

Proof of Theorem genpassl Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		prop 7184	. . . . . . . . 9 ⊢ (𝐴 ∈ P → ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∈ P)
2		elprnql 7190	. . . . . . . . 9 ⊢ ((⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩ ∈ P ∧ 𝑓 ∈ (1^st ‘𝐴)) → 𝑓 ∈ Q)
3	1, 2	sylan 279	. . . . . . . 8 ⊢ ((𝐴 ∈ P ∧ 𝑓 ∈ (1^st ‘𝐴)) → 𝑓 ∈ Q)
4		prop 7184	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ P → ⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩ ∈ P)
5		elprnql 7190	. . . . . . . . . . . . . . . 16 ⊢ ((⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩ ∈ P ∧ 𝑔 ∈ (1^st ‘𝐵)) → 𝑔 ∈ Q)
6	4, 5	sylan 279	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ P ∧ 𝑔 ∈ (1^st ‘𝐵)) → 𝑔 ∈ Q)
7		r19.41v 2545	. . . . . . . . . . . . . . . . 17 ⊢ (∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))
8		prop 7184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 ∈ P → ⟨(1^st ‘𝐶), (2^nd ‘𝐶)⟩ ∈ P)
9		elprnql 7190	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨(1^st ‘𝐶), (2^nd ‘𝐶)⟩ ∈ P ∧ ℎ ∈ (1^st ‘𝐶)) → ℎ ∈ Q)
10	8, 9	sylan 279	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ P ∧ ℎ ∈ (1^st ‘𝐶)) → ℎ ∈ Q)
11		oveq2 5714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = (𝑔𝐺ℎ) → (𝑓𝐺𝑡) = (𝑓𝐺(𝑔𝐺ℎ)))
12	11	adantr 272	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = (𝑔𝐺ℎ) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q)) → (𝑓𝐺𝑡) = (𝑓𝐺(𝑔𝐺ℎ)))
13		genpassg.6	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ)))
14	13	adantl 273	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = (𝑔𝐺ℎ) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q)) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ)))
15	12, 14	eqtr4d 2135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = (𝑔𝐺ℎ) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q)) → (𝑓𝐺𝑡) = ((𝑓𝐺𝑔)𝐺ℎ))
16	15	eqeq2d 2111	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = (𝑔𝐺ℎ) ∧ (𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q)) → (𝑥 = (𝑓𝐺𝑡) ↔ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
17	16	expcom 115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → (𝑡 = (𝑔𝐺ℎ) → (𝑥 = (𝑓𝐺𝑡) ↔ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
18	17	pm5.32d 441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
19	18	3expa 1149	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 ∈ Q ∧ 𝑔 ∈ Q) ∧ ℎ ∈ Q) → ((𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
20	10, 19	sylan2 282	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 ∈ Q ∧ 𝑔 ∈ Q) ∧ (𝐶 ∈ P ∧ ℎ ∈ (1^st ‘𝐶))) → ((𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
21	20	anassrs 395	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓 ∈ Q ∧ 𝑔 ∈ Q) ∧ 𝐶 ∈ P) ∧ ℎ ∈ (1^st ‘𝐶)) → ((𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
22	21	rexbidva 2393	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∈ Q ∧ 𝑔 ∈ Q) ∧ 𝐶 ∈ P) → (∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ ∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
23	7, 22	syl5rbbr 194	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ Q ∧ 𝑔 ∈ Q) ∧ 𝐶 ∈ P) → (∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
24	23	an32s 538	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ Q ∧ 𝐶 ∈ P) ∧ 𝑔 ∈ Q) → (∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
25	6, 24	sylan2 282	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ Q ∧ 𝐶 ∈ P) ∧ (𝐵 ∈ P ∧ 𝑔 ∈ (1^st ‘𝐵))) → (∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
26	25	anassrs 395	. . . . . . . . . . . . 13 ⊢ ((((𝑓 ∈ Q ∧ 𝐶 ∈ P) ∧ 𝐵 ∈ P) ∧ 𝑔 ∈ (1^st ‘𝐵)) → (∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
27	26	rexbidva 2393	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ Q ∧ 𝐶 ∈ P) ∧ 𝐵 ∈ P) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ ∃𝑔 ∈ (1^st ‘𝐵)(∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
28		r19.41v 2545	. . . . . . . . . . . 12 ⊢ (∃𝑔 ∈ (1^st ‘𝐵)(∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡)))
29	27, 28	syl6bb 195	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ Q ∧ 𝐶 ∈ P) ∧ 𝐵 ∈ P) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
30	29	an31s 540	. . . . . . . . . 10 ⊢ (((𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ 𝑓 ∈ Q) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
31	30	exbidv 1764	. . . . . . . . 9 ⊢ (((𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ 𝑓 ∈ Q) → (∃𝑡∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ ∃𝑡(∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
32		genpelvl.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)
33	32	caovcl 5857	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ Q ∧ ℎ ∈ Q) → (𝑔𝐺ℎ) ∈ Q)
34		elisset 2655	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔𝐺ℎ) ∈ Q → ∃𝑡 𝑡 = (𝑔𝐺ℎ))
35	33, 34	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ Q ∧ ℎ ∈ Q) → ∃𝑡 𝑡 = (𝑔𝐺ℎ))
36	35	biantrurd 301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∈ Q ∧ ℎ ∈ Q) → (𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ (∃𝑡 𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
37		19.41v 1841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃𝑡 𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
38	36, 37	syl6bbr 197	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ∈ Q ∧ ℎ ∈ Q) → (𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
39	10, 38	sylan2 282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ∈ Q ∧ (𝐶 ∈ P ∧ ℎ ∈ (1^st ‘𝐶))) → (𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
40	39	anassrs 395	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔 ∈ Q ∧ 𝐶 ∈ P) ∧ ℎ ∈ (1^st ‘𝐶)) → (𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
41	40	rexbidva 2393	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ Q ∧ 𝐶 ∈ P) → (∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃ℎ ∈ (1^st ‘𝐶)∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
42		rexcom4 2664	. . . . . . . . . . . . . . . . 17 ⊢ (∃ℎ ∈ (1^st ‘𝐶)∃𝑡(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ ∃𝑡∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
43	41, 42	syl6bb 195	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ Q ∧ 𝐶 ∈ P) → (∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
44	43	ancoms 266	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ P ∧ 𝑔 ∈ Q) → (∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
45	6, 44	sylan2 282	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ P ∧ (𝐵 ∈ P ∧ 𝑔 ∈ (1^st ‘𝐵))) → (∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
46	45	anassrs 395	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ P ∧ 𝐵 ∈ P) ∧ 𝑔 ∈ (1^st ‘𝐵)) → (∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
47	46	rexbidva 2393	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ P ∧ 𝐵 ∈ P) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑔 ∈ (1^st ‘𝐵)∃𝑡∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
48	47	ancoms 266	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ P ∧ 𝐶 ∈ P) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑔 ∈ (1^st ‘𝐵)∃𝑡∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
49		rexcom4 2664	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ (1^st ‘𝐵)∃𝑡∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ ∃𝑡∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
50	48, 49	syl6bb 195	. . . . . . . . . 10 ⊢ ((𝐵 ∈ P ∧ 𝐶 ∈ P) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
51	50	adantr 272	. . . . . . . . 9 ⊢ (((𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ 𝑓 ∈ Q) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)(𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
52		df-rex 2381	. . . . . . . . . . 11 ⊢ (∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑡(𝑡 ∈ (1^st ‘(𝐵𝐹𝐶)) ∧ 𝑥 = (𝑓𝐺𝑡)))
53		genpelvl.1	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^st ‘𝑤) ∧ 𝑧 ∈ (1^st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^nd ‘𝑤) ∧ 𝑧 ∈ (2^nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)
54	53, 32	genpelvl 7221	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝑡 ∈ (1^st ‘(𝐵𝐹𝐶)) ↔ ∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ)))
55	54	anbi1d 456	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝑡 ∈ (1^st ‘(𝐵𝐹𝐶)) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
56	55	exbidv 1764	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ P ∧ 𝐶 ∈ P) → (∃𝑡(𝑡 ∈ (1^st ‘(𝐵𝐹𝐶)) ∧ 𝑥 = (𝑓𝐺𝑡)) ↔ ∃𝑡(∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
57	52, 56	syl5bb 191	. . . . . . . . . 10 ⊢ ((𝐵 ∈ P ∧ 𝐶 ∈ P) → (∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑡(∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
58	57	adantr 272	. . . . . . . . 9 ⊢ (((𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ 𝑓 ∈ Q) → (∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑡(∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑡 = (𝑔𝐺ℎ) ∧ 𝑥 = (𝑓𝐺𝑡))))
59	31, 51, 58	3bitr4rd 220	. . . . . . . 8 ⊢ (((𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ 𝑓 ∈ Q) → (∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
60	3, 59	sylan2 282	. . . . . . 7 ⊢ (((𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 ∈ P ∧ 𝑓 ∈ (1^st ‘𝐴))) → (∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
61	60	anassrs 395	. . . . . 6 ⊢ ((((𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ 𝐴 ∈ P) ∧ 𝑓 ∈ (1^st ‘𝐴)) → (∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
62	61	rexbidva 2393	. . . . 5 ⊢ (((𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ 𝐴 ∈ P) → (∃𝑓 ∈ (1^st ‘𝐴)∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
63	62	ancoms 266	. . . 4 ⊢ ((𝐴 ∈ P ∧ (𝐵 ∈ P ∧ 𝐶 ∈ P)) → (∃𝑓 ∈ (1^st ‘𝐴)∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
64	63	3impb 1145	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (∃𝑓 ∈ (1^st ‘𝐴)∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡) ↔ ∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
65		genpassg.5	. . . . . 6 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓𝐹𝑔) ∈ P)
66	65	caovcl 5857	. . . . 5 ⊢ ((𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝐵𝐹𝐶) ∈ P)
67	53, 32	genpelvl 7221	. . . . 5 ⊢ ((𝐴 ∈ P ∧ (𝐵𝐹𝐶) ∈ P) → (𝑥 ∈ (1^st ‘(𝐴𝐹(𝐵𝐹𝐶))) ↔ ∃𝑓 ∈ (1^st ‘𝐴)∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡)))
68	66, 67	sylan2 282	. . . 4 ⊢ ((𝐴 ∈ P ∧ (𝐵 ∈ P ∧ 𝐶 ∈ P)) → (𝑥 ∈ (1^st ‘(𝐴𝐹(𝐵𝐹𝐶))) ↔ ∃𝑓 ∈ (1^st ‘𝐴)∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡)))
69	68	3impb 1145	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝑥 ∈ (1^st ‘(𝐴𝐹(𝐵𝐹𝐶))) ↔ ∃𝑓 ∈ (1^st ‘𝐴)∃𝑡 ∈ (1^st ‘(𝐵𝐹𝐶))𝑥 = (𝑓𝐺𝑡)))
70		df-rex 2381	. . . . 5 ⊢ (∃𝑡 ∈ (1^st ‘(𝐴𝐹𝐵))∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ) ↔ ∃𝑡(𝑡 ∈ (1^st ‘(𝐴𝐹𝐵)) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
71	53, 32	genpelvl 7221	. . . . . . . 8 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝑡 ∈ (1^st ‘(𝐴𝐹𝐵)) ↔ ∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔)))
72	71	3adant3 969	. . . . . . 7 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝑡 ∈ (1^st ‘(𝐴𝐹𝐵)) ↔ ∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔)))
73	72	anbi1d 456	. . . . . 6 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝑡 ∈ (1^st ‘(𝐴𝐹𝐵)) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
74	73	exbidv 1764	. . . . 5 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (∃𝑡(𝑡 ∈ (1^st ‘(𝐴𝐹𝐵)) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑡(∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
75	70, 74	syl5bb 191	. . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (∃𝑡 ∈ (1^st ‘(𝐴𝐹𝐵))∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ) ↔ ∃𝑡(∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
76	65	caovcl 5857	. . . . . 6 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴𝐹𝐵) ∈ P)
77	53, 32	genpelvl 7221	. . . . . 6 ⊢ (((𝐴𝐹𝐵) ∈ P ∧ 𝐶 ∈ P) → (𝑥 ∈ (1^st ‘((𝐴𝐹𝐵)𝐹𝐶)) ↔ ∃𝑡 ∈ (1^st ‘(𝐴𝐹𝐵))∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
78	76, 77	sylan 279	. . . . 5 ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ 𝐶 ∈ P) → (𝑥 ∈ (1^st ‘((𝐴𝐹𝐵)𝐹𝐶)) ↔ ∃𝑡 ∈ (1^st ‘(𝐴𝐹𝐵))∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
79	78	3impa 1144	. . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝑥 ∈ (1^st ‘((𝐴𝐹𝐵)𝐹𝐶)) ↔ ∃𝑡 ∈ (1^st ‘(𝐴𝐹𝐵))∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
80	32	caovcl 5857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q) → (𝑓𝐺𝑔) ∈ Q)
81		elisset 2655	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓𝐺𝑔) ∈ Q → ∃𝑡 𝑡 = (𝑓𝐺𝑔))
82	80, 81	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q) → ∃𝑡 𝑡 = (𝑓𝐺𝑔))
83	82	biantrurd 301	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q) → (∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ (∃𝑡 𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ))))
84		oveq1 5713	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = (𝑓𝐺𝑔) → (𝑡𝐺ℎ) = ((𝑓𝐺𝑔)𝐺ℎ))
85	84	eqeq2d 2111	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = (𝑓𝐺𝑔) → (𝑥 = (𝑡𝐺ℎ) ↔ 𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
86	85	rexbidv 2397	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = (𝑓𝐺𝑔) → (∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ) ↔ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
87	86	pm5.32i 445	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
88	87	exbii 1552	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
89		19.41v 1841	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)) ↔ (∃𝑡 𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
90	88, 89	bitri 183	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (∃𝑡 𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
91	83, 90	syl6bbr 197	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q) → (∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
92	6, 91	sylan2 282	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ Q ∧ (𝐵 ∈ P ∧ 𝑔 ∈ (1^st ‘𝐵))) → (∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
93	92	anassrs 395	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ Q ∧ 𝐵 ∈ P) ∧ 𝑔 ∈ (1^st ‘𝐵)) → (∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
94	93	rexbidva 2393	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ Q ∧ 𝐵 ∈ P) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑔 ∈ (1^st ‘𝐵)∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
95		rexcom4 2664	. . . . . . . . . . . . 13 ⊢ (∃𝑔 ∈ (1^st ‘𝐵)∃𝑡(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑡∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
96	94, 95	syl6bb 195	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ Q ∧ 𝐵 ∈ P) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
97	96	ancoms 266	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ P ∧ 𝑓 ∈ Q) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
98	3, 97	sylan2 282	. . . . . . . . . 10 ⊢ ((𝐵 ∈ P ∧ (𝐴 ∈ P ∧ 𝑓 ∈ (1^st ‘𝐴))) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
99	98	anassrs 395	. . . . . . . . 9 ⊢ (((𝐵 ∈ P ∧ 𝐴 ∈ P) ∧ 𝑓 ∈ (1^st ‘𝐴)) → (∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
100	99	rexbidva 2393	. . . . . . . 8 ⊢ ((𝐵 ∈ P ∧ 𝐴 ∈ P) → (∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑓 ∈ (1^st ‘𝐴)∃𝑡∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
101		rexcom4 2664	. . . . . . . 8 ⊢ (∃𝑓 ∈ (1^st ‘𝐴)∃𝑡∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑡∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
102	100, 101	syl6bb 195	. . . . . . 7 ⊢ ((𝐵 ∈ P ∧ 𝐴 ∈ P) → (∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
103		r19.41v 2545	. . . . . . . . . 10 ⊢ (∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
104	103	rexbii 2401	. . . . . . . . 9 ⊢ (∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑓 ∈ (1^st ‘𝐴)(∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
105		r19.41v 2545	. . . . . . . . 9 ⊢ (∃𝑓 ∈ (1^st ‘𝐴)(∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
106	104, 105	bitri 183	. . . . . . . 8 ⊢ (∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ (∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
107	106	exbii 1552	. . . . . . 7 ⊢ (∃𝑡∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)(𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)) ↔ ∃𝑡(∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ)))
108	102, 107	syl6bb 195	. . . . . 6 ⊢ ((𝐵 ∈ P ∧ 𝐴 ∈ P) → (∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
109	108	ancoms 266	. . . . 5 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
110	109	3adant3 969	. . . 4 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ) ↔ ∃𝑡(∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)𝑡 = (𝑓𝐺𝑔) ∧ ∃ℎ ∈ (1^st ‘𝐶)𝑥 = (𝑡𝐺ℎ))))
111	75, 79, 110	3bitr4d 219	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝑥 ∈ (1^st ‘((𝐴𝐹𝐵)𝐹𝐶)) ↔ ∃𝑓 ∈ (1^st ‘𝐴)∃𝑔 ∈ (1^st ‘𝐵)∃ℎ ∈ (1^st ‘𝐶)𝑥 = ((𝑓𝐺𝑔)𝐺ℎ)))
112	64, 69, 111	3bitr4rd 220	. 2 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝑥 ∈ (1^st ‘((𝐴𝐹𝐵)𝐹𝐶)) ↔ 𝑥 ∈ (1^st ‘(𝐴𝐹(𝐵𝐹𝐶)))))
113	112	eqrdv 2098	1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (1^st ‘((𝐴𝐹𝐵)𝐹𝐶)) = (1^st ‘(𝐴𝐹(𝐵𝐹𝐶))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 930 = wceq 1299 ∃wex 1436 ∈ wcel 1448 ∃wrex 2376 {crab 2379 ⟨cop 3477 × cxp 4475 dom cdm 4477 ‘cfv 5059 (class class class)co 5706 ∈ cmpo 5708 1^st c1st 5967 2^nd c2nd 5968 Qcnq 6989 Pcnp 7000

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-13 1459 ax-14 1460 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-coll 3983 ax-sep 3986 ax-pow 4038 ax-pr 4069 ax-un 4293 ax-setind 4390 ax-iinf 4440

This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-fal 1305 df-nf 1405 df-sb 1704 df-eu 1963 df-mo 1964 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ne 2268 df-ral 2380 df-rex 2381 df-reu 2382 df-rab 2384 df-v 2643 df-sbc 2863 df-csb 2956 df-dif 3023 df-un 3025 df-in 3027 df-ss 3034 df-pw 3459 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-int 3719 df-iun 3762 df-br 3876 df-opab 3930 df-mpt 3931 df-id 4153 df-iom 4443 df-xp 4483 df-rel 4484 df-cnv 4485 df-co 4486 df-dm 4487 df-rn 4488 df-res 4489 df-ima 4490 df-iota 5024 df-fun 5061 df-fn 5062 df-f 5063 df-f1 5064 df-fo 5065 df-f1o 5066 df-fv 5067 df-ov 5709 df-oprab 5710 df-mpo 5711 df-1st 5969 df-2nd 5970 df-qs 6365 df-ni 7013 df-nqqs 7057 df-inp 7175

This theorem is referenced by: genpassg 7235

W3C validator