Description: The indexed union of connected overlapping subspaces sharing a common
point is connected. The proof of iunconALTVD is a Virtual Deduction proof of based on Mario Carneiro's proof of iuncon 17154. The proof of
iunconALTVD is verified by automatically transforming it into the Metamath proof of iunconALT 28774 using completeusersproof, which is
verified by the Metamath program. (Contributed by
Alan Sare, 9-Apr-2018.)
Hypotheses
| Ref
| Expression |
|---|
| iunconaltvd.2 |
⊢ ( 𝜑 ▶ 𝐽 ∈ (TopOn‘𝑋) ) |
| iunconaltvd.3 |
⊢ ( ( 𝜑 , 𝑘 ∈ 𝐴 ) ▶ 𝐵 ⊆ 𝑋 ) |
| iunconaltvd.4 |
⊢ ( ( 𝜑 , 𝑘 ∈ 𝐴 ) ▶ 𝑃 ∈ 𝐵 ) |
| iunconaltvd.5 |
⊢ ( ( 𝜑 , 𝑘 ∈ 𝐴 ) ▶ (𝐽 ↾t 𝐵) ∈ Con ) |
Assertion
| Ref
| Expression |
|---|
| iunconALTVD |
⊢ ( 𝜑 ▶ (𝐽 ↾t ∪ 𝑘
∈ 𝐴 𝐵) ∈ Con ) |
Distinct variable groups: 𝜑,𝑘 𝐴,𝑘 𝑘,𝐽 𝑃,𝑘 𝑘,𝑋
Allowed substitution hint: 𝐵(𝑘)
Proof of Theorem iunconALTVD
| Step | Hyp | Expression |
|---|
| h1 | | ⊢ ( 𝜑 ▶ 𝐽 ∈ (TopOn‘𝑋) )
| | h2 | | ⊢ ( ( 𝜑 , 𝑘 ∈ 𝐴 ) ▶ 𝐵 ⊆ 𝑋 )
| | h3 | | ⊢ ( ( 𝜑 , 𝑘 ∈ 𝐴 ) ▶ 𝑃 ∈ 𝐵 )
| | h4 | | ⊢ ( ( 𝜑 , 𝑘 ∈ 𝐴 ) ▶ (𝐽 ↾t 𝐵) ∈ Con )
| | 5 | | ⊢ (((((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐽) ∧ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅) ∧ (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅) ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)) ∧ ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)) ↔ ( 𝜑 , 𝑢 ∈ 𝐽 , 𝑣 ∈ 𝐽 , (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ , (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ , (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵) , ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣) ))
| | qed | 1,2,3,4,5 | ⊢ ( 𝜑 ▶ (𝐽 ↾t ∪ 𝑘 ∈ 𝐴𝐵) ∈ Con )
| |