Step
*
1
1
of Lemma
all-quotient-true3
1. T : Type@i'
2. f : T ⟶ Base@i
3. ∀x:T. ((f x) = x ∈ T)@i
4. P : T ⟶ ℙ@i'
5. ∀t:T ⋂ Base. ⇃(P[t])
⇐⇒ ⇃(∀t:T ⋂ Base. P[t])
⊢ ∀t:T. ⇃(P[t])
⇐⇒ ⇃(∀t:T. P[t])
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }
1
1. T : Type@i'
2. f : T ⟶ Base@i
3. ∀x:T. ((f x) = x ∈ T)@i
4. P : T ⟶ ℙ@i'
5. ∀t:T ⋂ Base. ⇃(P[t])
⇐⇒ ⇃(∀t:T ⋂ Base. P[t])
6. ∀t:T. ⇃(P[t])@i
⊢ ⇃(∀t:T. P[t])
2
1. T : Type@i'
2. f : T ⟶ Base@i
3. ∀x:T. ((f x) = x ∈ T)@i
4. P : T ⟶ ℙ@i'
5. ∀t:T ⋂ Base. ⇃(P[t])
⇐⇒ ⇃(∀t:T ⋂ Base. P[t])
6. ⇃(∀t:T. P[t])@i
⊢ ∀t:T. ⇃(P[t])
Latex:
Latex:
1. T : Type@i'
2. f : T {}\mrightarrow{} Base@i
3. \mforall{}x:T. ((f x) = x)@i
4. P : T {}\mrightarrow{} \mBbbP{}@i'
5. \mforall{}t:T \mcap{} Base. \00D9(P[t]) \mLeftarrow{}{}\mRightarrow{} \00D9(\mforall{}t:T \mcap{} Base. P[t])
\mvdash{} \mforall{}t:T. \00D9(P[t]) \mLeftarrow{}{}\mRightarrow{} \00D9(\mforall{}t:T. P[t])
By
Latex:
RepeatFor 2 ((D 0 THENA Auto))
Home
Index