genpassg - Intuitionistic Logic Explorer

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

Theorem genpassg 7724

Description: Associativity of an operation on reals. (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
genpassg	⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)))

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

**Proof of Theorem genpassg**
Step	Hyp	Ref	Expression
1		genpelvl.1	. . 3 ⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^st ‘𝑤) ∧ 𝑧 ∈ (1^st ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^nd ‘𝑤) ∧ 𝑧 ∈ (2^nd ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩)
2		genpelvl.2	. . 3 ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q)
3		genpassg.4	. . 3 ⊢ dom 𝐹 = (P × P)
4		genpassg.5	. . 3 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓𝐹𝑔) ∈ P)
5		genpassg.6	. . 3 ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ)))
6	1, 2, 3, 4, 5	genpassl 7722	. 2 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (1^st ‘((𝐴𝐹𝐵)𝐹𝐶)) = (1^st ‘(𝐴𝐹(𝐵𝐹𝐶))))
7	1, 2, 3, 4, 5	genpassu 7723	. 2 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (2^nd ‘((𝐴𝐹𝐵)𝐹𝐶)) = (2^nd ‘(𝐴𝐹(𝐵𝐹𝐶))))
8	4	caovcl 6166	. . . . 5 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴𝐹𝐵) ∈ P)
9	4	caovcl 6166	. . . . 5 ⊢ (((𝐴𝐹𝐵) ∈ P ∧ 𝐶 ∈ P) → ((𝐴𝐹𝐵)𝐹𝐶) ∈ P)
10	8, 9	sylan 283	. . . 4 ⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ 𝐶 ∈ P) → ((𝐴𝐹𝐵)𝐹𝐶) ∈ P)
11	10	3impa 1218	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴𝐹𝐵)𝐹𝐶) ∈ P)
12	4	caovcl 6166	. . . . 5 ⊢ ((𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝐵𝐹𝐶) ∈ P)
13	4	caovcl 6166	. . . . 5 ⊢ ((𝐴 ∈ P ∧ (𝐵𝐹𝐶) ∈ P) → (𝐴𝐹(𝐵𝐹𝐶)) ∈ P)
14	12, 13	sylan2 286	. . . 4 ⊢ ((𝐴 ∈ P ∧ (𝐵 ∈ P ∧ 𝐶 ∈ P)) → (𝐴𝐹(𝐵𝐹𝐶)) ∈ P)
15	14	3impb 1223	. . 3 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝐴𝐹(𝐵𝐹𝐶)) ∈ P)
16		preqlu 7670	. . 3 ⊢ ((((𝐴𝐹𝐵)𝐹𝐶) ∈ P ∧ (𝐴𝐹(𝐵𝐹𝐶)) ∈ P) → (((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)) ↔ ((1^st ‘((𝐴𝐹𝐵)𝐹𝐶)) = (1^st ‘(𝐴𝐹(𝐵𝐹𝐶))) ∧ (2^nd ‘((𝐴𝐹𝐵)𝐹𝐶)) = (2^nd ‘(𝐴𝐹(𝐵𝐹𝐶))))))
17	11, 15, 16	syl2anc 411	. 2 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)) ↔ ((1^st ‘((𝐴𝐹𝐵)𝐹𝐶)) = (1^st ‘(𝐴𝐹(𝐵𝐹𝐶))) ∧ (2^nd ‘((𝐴𝐹𝐵)𝐹𝐶)) = (2^nd ‘(𝐴𝐹(𝐵𝐹𝐶))))))
18	6, 7, 17	mpbir2and 950	1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 1002 = wceq 1395 ∈ wcel 2200 ∃wrex 2509 {crab 2512 ⟨cop 3669 × cxp 4717 dom cdm 4719 ‘cfv 5318 (class class class)co 6007 ∈ cmpo 6009 1^st c1st 6290 2^nd c2nd 6291 Qcnq 7478 Pcnp 7489

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4199 ax-sep 4202 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-setind 4629 ax-iinf 4680

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-ral 2513 df-rex 2514 df-reu 2515 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-int 3924 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-id 4384 df-iom 4683 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-res 4731 df-ima 4732 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-f1 5323 df-fo 5324 df-f1o 5325 df-fv 5326 df-ov 6010 df-oprab 6011 df-mpo 6012 df-1st 6292 df-2nd 6293 df-qs 6694 df-ni 7502 df-nqqs 7546 df-inp 7664

This theorem is referenced by: addassprg 7777 mulassprg 7779

W3C validator