Theorem chirredlem3 30445

Description: Lemma for chirredi 30447. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)

Hypotheses

Ref	Expression
chirred.1	⊢ 𝐴 ∈ Cℋ
chirred.2	⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥)

Assertion

Ref	Expression
chirredlem3	⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝))

Distinct variable group:   𝑞,𝑝,𝑟,𝑥,𝐴

Proof of Theorem chirredlem3

Step	Hyp	Ref	Expression
1		atelch 30397	. . 3 ⊢ (𝑞 ∈ HAtoms → 𝑞 ∈ Cℋ )
2		chirred.1	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ Cℋ
3	2	chirredlem2 30444	. . . . . . . . . . 11 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞)) = 𝑞)
4	3	oveq2d 7218	. . . . . . . . . 10 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑟 ∨ℋ 𝑞))
5		atelch 30397	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ HAtoms → 𝑟 ∈ Cℋ )
6	5	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → 𝑟 ∈ Cℋ )
7		atelch 30397	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ HAtoms → 𝑝 ∈ Cℋ )
8		chjcl 29410	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → (𝑝 ∨ℋ 𝑞) ∈ Cℋ )
9	7, 8	sylan 583	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) → (𝑝 ∨ℋ 𝑞) ∈ Cℋ )
10	9	ad2ant2r 747	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) → (𝑝 ∨ℋ 𝑞) ∈ Cℋ )
11		id 22	. . . . . . . . . . . . 13 ⊢ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))
12		pjoml2 29664	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ Cℋ ∧ (𝑝 ∨ℋ 𝑞) ∈ Cℋ ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞))
13	6, 10, 11, 12	syl3an 1162	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ ((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞))
14	13	3com12 1125	. . . . . . . . . . 11 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞))
15	14	3expb 1122	. . . . . . . . . 10 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞))
16	4, 15	eqtr3d 2776	. . . . . . . . 9 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ 𝑞) = (𝑝 ∨ℋ 𝑞))
17	16	ineq2d 4117	. . . . . . . 8 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = (𝐴 ∩ (𝑝 ∨ℋ 𝑞)))
18		breq2 5047	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑟 → (𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑟))
19		chirred.2	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥)
20	18, 19	vtoclga 3482	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ Cℋ → 𝐴 𝐶ℋ 𝑟)
21		breq2 5047	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑞 → (𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑞))
22	21, 19	vtoclga 3482	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ Cℋ → 𝐴 𝐶ℋ 𝑞)
23	20, 22	anim12i 616	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞))
24		fh1 29671	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Cℋ ∧ 𝑟 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ (𝐴 𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)))
25	2, 24	mp3anl1 1457	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ (𝐴 𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)))
26	23, 25	mpdan 687	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)))
27	5, 26	sylan 583	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)))
28	27	ancoms 462	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ Cℋ ∧ 𝑟 ∈ HAtoms) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)))
29	28	adantrr 717	. . . . . . . . . 10 ⊢ ((𝑞 ∈ Cℋ ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴)) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)))
30	29	ad2ant2r 747	. . . . . . . . 9 ⊢ (((𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)))
31	30	adantll 714	. . . . . . . 8 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)))
32		breq2 5047	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑝 → (𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑝))
33	32, 19	vtoclga 3482	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ Cℋ → 𝐴 𝐶ℋ 𝑝)
34	33, 22	anim12i 616	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞))
35		fh1 29671	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ (𝐴 𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞)))
36	2, 35	mp3anl1 1457	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) ∧ (𝐴 𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞)))
37	34, 36	mpdan 687	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞)))
38	7, 37	sylan 583	. . . . . . . . . 10 ⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞)))
39	38	ad2ant2r 747	. . . . . . . . 9 ⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞)))
40	39	adantr 484	. . . . . . . 8 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞)))
41	17, 31, 40	3eqtr3d 2782	. . . . . . 7 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞)))
42		sseqin2 4120	. . . . . . . . . . 11 ⊢ (𝑟 ⊆ 𝐴 ↔ (𝐴 ∩ 𝑟) = 𝑟)
43	42	biimpi 219	. . . . . . . . . 10 ⊢ (𝑟 ⊆ 𝐴 → (𝐴 ∩ 𝑟) = 𝑟)
44	43	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝐴 ∩ 𝑟) = 𝑟)
45	44	adantl 485	. . . . . . . 8 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ 𝑟) = 𝑟)
46		incom 4105	. . . . . . . . . 10 ⊢ (𝐴 ∩ 𝑞) = (𝑞 ∩ 𝐴)
47		chsh 29277	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ Cℋ → 𝑞 ∈ Sℋ )
48	2	chshii 29280	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ Sℋ
49		orthin 29499	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ Sℋ ∧ 𝐴 ∈ Sℋ ) → (𝑞 ⊆ (⊥‘𝐴) → (𝑞 ∩ 𝐴) = 0ℋ))
50	47, 48, 49	sylancl 589	. . . . . . . . . . 11 ⊢ (𝑞 ∈ Cℋ → (𝑞 ⊆ (⊥‘𝐴) → (𝑞 ∩ 𝐴) = 0ℋ))
51	50	imp 410	. . . . . . . . . 10 ⊢ ((𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) → (𝑞 ∩ 𝐴) = 0ℋ)
52	46, 51	syl5eq 2786	. . . . . . . . 9 ⊢ ((𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) → (𝐴 ∩ 𝑞) = 0ℋ)
53	52	ad2antlr 727	. . . . . . . 8 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ 𝑞) = 0ℋ)
54	45, 53	oveq12d 7220	. . . . . . 7 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)) = (𝑟 ∨ℋ 0ℋ))
55		sseqin2 4120	. . . . . . . . . . 11 ⊢ (𝑝 ⊆ 𝐴 ↔ (𝐴 ∩ 𝑝) = 𝑝)
56	55	biimpi 219	. . . . . . . . . 10 ⊢ (𝑝 ⊆ 𝐴 → (𝐴 ∩ 𝑝) = 𝑝)
57	56	adantl 485	. . . . . . . . 9 ⊢ ((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) → (𝐴 ∩ 𝑝) = 𝑝)
58	57	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ 𝑝) = 𝑝)
59	58, 53	oveq12d 7220	. . . . . . 7 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞)) = (𝑝 ∨ℋ 0ℋ))
60	41, 54, 59	3eqtr3d 2782	. . . . . 6 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ 0ℋ) = (𝑝 ∨ℋ 0ℋ))
61		chj0 29550	. . . . . . . . 9 ⊢ (𝑟 ∈ Cℋ → (𝑟 ∨ℋ 0ℋ) = 𝑟)
62	5, 61	syl 17	. . . . . . . 8 ⊢ (𝑟 ∈ HAtoms → (𝑟 ∨ℋ 0ℋ) = 𝑟)
63	62	ad2antrr 726	. . . . . . 7 ⊢ (((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ 0ℋ) = 𝑟)
64	63	adantl 485	. . . . . 6 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ 0ℋ) = 𝑟)
65		chj0 29550	. . . . . . . 8 ⊢ (𝑝 ∈ Cℋ → (𝑝 ∨ℋ 0ℋ) = 𝑝)
66	7, 65	syl 17	. . . . . . 7 ⊢ (𝑝 ∈ HAtoms → (𝑝 ∨ℋ 0ℋ) = 𝑝)
67	66	ad3antrrr 730	. . . . . 6 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑝 ∨ℋ 0ℋ) = 𝑝)
68	60, 64, 67	3eqtr3d 2782	. . . . 5 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → 𝑟 = 𝑝)
69	68	exp44 441	. . . 4 ⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) → (𝑟 ∈ HAtoms → (𝑟 ⊆ 𝐴 → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → 𝑟 = 𝑝))))
70	69	com34 91	. . 3 ⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) → (𝑟 ∈ HAtoms → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝))))
71	1, 70	sylanr1 682	. 2 ⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → (𝑟 ∈ HAtoms → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝))))
72	71	imp32 422	1 ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110   ∩ cin 3856   ⊆ wss 3857   class class class wbr 5043  ‘cfv 6369  (class class class)co 7202   S_ℋ csh 28981   C_ℋ cch 28982  ⊥cort 28983   ∨_ℋ chj 28986  0_ℋc0h 28988   𝐶_ℋ ccm 28989  HAtomscat 29018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-rep 5168  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512  ax-inf2 9245  ax-cc 10032  ax-cnex 10768  ax-resscn 10769  ax-1cn 10770  ax-icn 10771  ax-addcl 10772  ax-addrcl 10773  ax-mulcl 10774  ax-mulrcl 10775  ax-mulcom 10776  ax-addass 10777  ax-mulass 10778  ax-distr 10779  ax-i2m1 10780  ax-1ne0 10781  ax-1rid 10782  ax-rnegex 10783  ax-rrecex 10784  ax-cnre 10785  ax-pre-lttri 10786  ax-pre-lttrn 10787  ax-pre-ltadd 10788  ax-pre-mulgt0 10789  ax-pre-sup 10790  ax-addf 10791  ax-mulf 10792  ax-hilex 29052  ax-hfvadd 29053  ax-hvcom 29054  ax-hvass 29055  ax-hv0cl 29056  ax-hvaddid 29057  ax-hfvmul 29058  ax-hvmulid 29059  ax-hvmulass 29060  ax-hvdistr1 29061  ax-hvdistr2 29062  ax-hvmul0 29063  ax-hfi 29132  ax-his1 29135  ax-his2 29136  ax-his3 29137  ax-his4 29138  ax-hcompl 29255

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-pss 3876  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-tp 4536  df-op 4538  df-uni 4810  df-int 4850  df-iun 4896  df-iin 4897  df-br 5044  df-opab 5106  df-mpt 5125  df-tr 5151  df-id 5444  df-eprel 5449  df-po 5457  df-so 5458  df-fr 5498  df-se 5499  df-we 5500  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-pred 6149  df-ord 6205  df-on 6206  df-lim 6207  df-suc 6208  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-isom 6378  df-riota 7159  df-ov 7205  df-oprab 7206  df-mpo 7207  df-of 7458  df-om 7634  df-1st 7750  df-2nd 7751  df-supp 7893  df-wrecs 8036  df-recs 8097  df-rdg 8135  df-1o 8191  df-2o 8192  df-oadd 8195  df-omul 8196  df-er 8380  df-map 8499  df-pm 8500  df-ixp 8568  df-en 8616  df-dom 8617  df-sdom 8618  df-fin 8619  df-fsupp 8975  df-fi 9016  df-sup 9047  df-inf 9048  df-oi 9115  df-card 9538  df-acn 9541  df-pnf 10852  df-mnf 10853  df-xr 10854  df-ltxr 10855  df-le 10856  df-sub 11047  df-neg 11048  df-div 11473  df-nn 11814  df-2 11876  df-3 11877  df-4 11878  df-5 11879  df-6 11880  df-7 11881  df-8 11882  df-9 11883  df-n0 12074  df-z 12160  df-dec 12277  df-uz 12422  df-q 12528  df-rp 12570  df-xneg 12687  df-xadd 12688  df-xmul 12689  df-ioo 12922  df-ico 12924  df-icc 12925  df-fz 13079  df-fzo 13222  df-fl 13350  df-seq 13558  df-exp 13619  df-hash 13880  df-cj 14645  df-re 14646  df-im 14647  df-sqrt 14781  df-abs 14782  df-clim 15032  df-rlim 15033  df-sum 15233  df-struct 16686  df-ndx 16687  df-slot 16688  df-base 16690  df-sets 16691  df-ress 16692  df-plusg 16780  df-mulr 16781  df-starv 16782  df-sca 16783  df-vsca 16784  df-ip 16785  df-tset 16786  df-ple 16787  df-ds 16789  df-unif 16790  df-hom 16791  df-cco 16792  df-rest 16899  df-topn 16900  df-0g 16918  df-gsum 16919  df-topgen 16920  df-pt 16921  df-prds 16924  df-xrs 16979  df-qtop 16984  df-imas 16985  df-xps 16987  df-mre 17061  df-mrc 17062  df-acs 17064  df-mgm 18086  df-sgrp 18135  df-mnd 18146  df-submnd 18191  df-mulg 18461  df-cntz 18683  df-cmn 19144  df-psmet 20327  df-xmet 20328  df-met 20329  df-bl 20330  df-mopn 20331  df-fbas 20332  df-fg 20333  df-cnfld 20336  df-top 21763  df-topon 21780  df-topsp 21802  df-bases 21815  df-cld 21888  df-ntr 21889  df-cls 21890  df-nei 21967  df-cn 22096  df-cnp 22097  df-lm 22098  df-haus 22184  df-tx 22431  df-hmeo 22624  df-fil 22715  df-fm 22807  df-flim 22808  df-flf 22809  df-xms 23190  df-ms 23191  df-tms 23192  df-cfil 24124  df-cau 24125  df-cmet 24126  df-grpo 28546  df-gid 28547  df-ginv 28548  df-gdiv 28549  df-ablo 28598  df-vc 28612  df-nv 28645  df-va 28648  df-ba 28649  df-sm 28650  df-0v 28651  df-vs 28652  df-nmcv 28653  df-ims 28654  df-dip 28754  df-ssp 28775  df-ph 28866  df-cbn 28916  df-hnorm 29021  df-hba 29022  df-hvsub 29024  df-hlim 29025  df-hcau 29026  df-sh 29260  df-ch 29274  df-oc 29305  df-ch0 29306  df-shs 29361  df-span 29362  df-chj 29363  df-chsup 29364  df-pjh 29448  df-cm 29636  df-cv 30332  df-at 30391

This theorem is referenced by:  chirredlem4  30446