Theorem cvlexch1 36965

Description: An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.)

Hypotheses

Ref	Expression
cvlexch.b	⊢ 𝐵 = (Base‘𝐾)
cvlexch.l	⊢ ≤ = (le‘𝐾)
cvlexch.j	⊢ ∨ = (join‘𝐾)
cvlexch.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
cvlexch1	⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))

Proof of Theorem cvlexch1

Dummy variables 𝑞 𝑝 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvlexch.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
2		cvlexch.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
3		cvlexch.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
4		cvlexch.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
5	1, 2, 3, 4	iscvlat 36960	. . . . 5 ⊢ (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝))))
6	5	simprbi 500	. . . 4 ⊢ (𝐾 ∈ CvLat → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝)))
7		breq1 5033	. . . . . . . 8 ⊢ (𝑝 = 𝑃 → (𝑝 ≤ 𝑥 ↔ 𝑃 ≤ 𝑥))
8	7	notbid 321	. . . . . . 7 ⊢ (𝑝 = 𝑃 → (¬ 𝑝 ≤ 𝑥 ↔ ¬ 𝑃 ≤ 𝑥))
9		breq1 5033	. . . . . . 7 ⊢ (𝑝 = 𝑃 → (𝑝 ≤ (𝑥 ∨ 𝑞) ↔ 𝑃 ≤ (𝑥 ∨ 𝑞)))
10	8, 9	anbi12d 634	. . . . . 6 ⊢ (𝑝 = 𝑃 → ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) ↔ (¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ (𝑥 ∨ 𝑞))))
11		oveq2 7178	. . . . . . 7 ⊢ (𝑝 = 𝑃 → (𝑥 ∨ 𝑝) = (𝑥 ∨ 𝑃))
12	11	breq2d 5042	. . . . . 6 ⊢ (𝑝 = 𝑃 → (𝑞 ≤ (𝑥 ∨ 𝑝) ↔ 𝑞 ≤ (𝑥 ∨ 𝑃)))
13	10, 12	imbi12d 348	. . . . 5 ⊢ (𝑝 = 𝑃 → (((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝)) ↔ ((¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑃))))
14		oveq2 7178	. . . . . . . 8 ⊢ (𝑞 = 𝑄 → (𝑥 ∨ 𝑞) = (𝑥 ∨ 𝑄))
15	14	breq2d 5042	. . . . . . 7 ⊢ (𝑞 = 𝑄 → (𝑃 ≤ (𝑥 ∨ 𝑞) ↔ 𝑃 ≤ (𝑥 ∨ 𝑄)))
16	15	anbi2d 632	. . . . . 6 ⊢ (𝑞 = 𝑄 → ((¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ (𝑥 ∨ 𝑞)) ↔ (¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ (𝑥 ∨ 𝑄))))
17		breq1 5033	. . . . . 6 ⊢ (𝑞 = 𝑄 → (𝑞 ≤ (𝑥 ∨ 𝑃) ↔ 𝑄 ≤ (𝑥 ∨ 𝑃)))
18	16, 17	imbi12d 348	. . . . 5 ⊢ (𝑞 = 𝑄 → (((¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑃)) ↔ ((¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ (𝑥 ∨ 𝑄)) → 𝑄 ≤ (𝑥 ∨ 𝑃))))
19		breq2 5034	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑃 ≤ 𝑥 ↔ 𝑃 ≤ 𝑋))
20	19	notbid 321	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (¬ 𝑃 ≤ 𝑥 ↔ ¬ 𝑃 ≤ 𝑋))
21		oveq1 7177	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑥 ∨ 𝑄) = (𝑋 ∨ 𝑄))
22	21	breq2d 5042	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑃 ≤ (𝑥 ∨ 𝑄) ↔ 𝑃 ≤ (𝑋 ∨ 𝑄)))
23	20, 22	anbi12d 634	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ (𝑥 ∨ 𝑄)) ↔ (¬ 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))))
24		oveq1 7177	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑥 ∨ 𝑃) = (𝑋 ∨ 𝑃))
25	24	breq2d 5042	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑄 ≤ (𝑥 ∨ 𝑃) ↔ 𝑄 ≤ (𝑋 ∨ 𝑃)))
26	23, 25	imbi12d 348	. . . . 5 ⊢ (𝑥 = 𝑋 → (((¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ (𝑥 ∨ 𝑄)) → 𝑄 ≤ (𝑥 ∨ 𝑃)) ↔ ((¬ 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → 𝑄 ≤ (𝑋 ∨ 𝑃))))
27	13, 18, 26	rspc3v 3539	. . . 4 ⊢ ((𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝)) → ((¬ 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → 𝑄 ≤ (𝑋 ∨ 𝑃))))
28	6, 27	mpan9 510	. . 3 ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵)) → ((¬ 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → 𝑄 ≤ (𝑋 ∨ 𝑃)))
29	28	exp4b 434	. 2 ⊢ (𝐾 ∈ CvLat → ((𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (¬ 𝑃 ≤ 𝑋 → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))))
30	29	3imp 1112	1 ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1088   = wceq 1542   ∈ wcel 2114  ∀wral 3053   class class class wbr 5030  ‘cfv 6339  (class class class)co 7170  Basecbs 16586  lecple 16675  joincjn 17670  Atomscatm 36900  AtLatcal 36901  CvLatclc 36902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rab 3062  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-iota 6297  df-fv 6347  df-ov 7173  df-cvlat 36959

This theorem is referenced by:  cvlexch2  36966  cvlexchb1  36967  cvlexch3  36969  cvlcvr1  36976  hlexch1  37019