Metamath Proof Explorer

Theorem ispsubsp2

Description: The predicate "is a projective subspace". (Contributed by NM, 13-Jan-2012)

Ref Expression
Hypotheses psubspset.l ⊢≤˙=≤K
psubspset.j ⊢∨˙=join⁡K
psubspset.a ⊢A=Atoms⁡K
psubspset.s ⊢S=PSubSp⁡K
Assertion ispsubsp2 ⊢K∈D→X∈S↔X⊆A∧∀p∈A∃q∈X∃r∈Xp≤˙q∨˙r→p∈X

Proof

Step Hyp Ref Expression
1 psubspset.l ⊢≤˙=≤K
2 psubspset.j ⊢∨˙=join⁡K
3 psubspset.a ⊢A=Atoms⁡K
4 psubspset.s ⊢S=PSubSp⁡K
5 1 2 3 4 ispsubsp ⊢K∈D→X∈S↔X⊆A∧∀q∈X∀r∈X∀p∈Ap≤˙q∨˙r→p∈X
6 ralcom ⊢∀r∈X∀p∈Ap≤˙q∨˙r→p∈X↔∀p∈A∀r∈Xp≤˙q∨˙r→p∈X
7 r19.23v ⊢∀r∈Xp≤˙q∨˙r→p∈X↔∃r∈Xp≤˙q∨˙r→p∈X
8 7 ralbii ⊢∀p∈A∀r∈Xp≤˙q∨˙r→p∈X↔∀p∈A∃r∈Xp≤˙q∨˙r→p∈X
9 6 8 bitri ⊢∀r∈X∀p∈Ap≤˙q∨˙r→p∈X↔∀p∈A∃r∈Xp≤˙q∨˙r→p∈X
10 9 ralbii ⊢∀q∈X∀r∈X∀p∈Ap≤˙q∨˙r→p∈X↔∀q∈X∀p∈A∃r∈Xp≤˙q∨˙r→p∈X
11 ralcom ⊢∀q∈X∀p∈A∃r∈Xp≤˙q∨˙r→p∈X↔∀p∈A∀q∈X∃r∈Xp≤˙q∨˙r→p∈X
12 r19.23v ⊢∀q∈X∃r∈Xp≤˙q∨˙r→p∈X↔∃q∈X∃r∈Xp≤˙q∨˙r→p∈X
13 12 ralbii ⊢∀p∈A∀q∈X∃r∈Xp≤˙q∨˙r→p∈X↔∀p∈A∃q∈X∃r∈Xp≤˙q∨˙r→p∈X
14 11 13 bitri ⊢∀q∈X∀p∈A∃r∈Xp≤˙q∨˙r→p∈X↔∀p∈A∃q∈X∃r∈Xp≤˙q∨˙r→p∈X
15 10 14 bitri ⊢∀q∈X∀r∈X∀p∈Ap≤˙q∨˙r→p∈X↔∀p∈A∃q∈X∃r∈Xp≤˙q∨˙r→p∈X
16 15 a1i ⊢K∈D→∀q∈X∀r∈X∀p∈Ap≤˙q∨˙r→p∈X↔∀p∈A∃q∈X∃r∈Xp≤˙q∨˙r→p∈X
17 16 anbi2d ⊢K∈D→X⊆A∧∀q∈X∀r∈X∀p∈Ap≤˙q∨˙r→p∈X↔X⊆A∧∀p∈A∃q∈X∃r∈Xp≤˙q∨˙r→p∈X
18 5 17 bitrd ⊢K∈D→X∈S↔X⊆A∧∀p∈A∃q∈X∃r∈Xp≤˙q∨˙r→p∈X