Theorem iunconALTVD
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
StepHypExpression
h1 (   𝜑   ▶   𝐽 ∈ (TopOn‘𝑋)   )
h2 (   (   𝜑   ,   𝑘𝐴   )   ▶   𝐵𝑋   )
h3 (   (   𝜑   ,   𝑘𝐴   )   ▶   𝑃𝐵   )
h4 (   (   𝜑   ,   𝑘𝐴   )   ▶   (𝐽t 𝐵) ∈ Con   )
5 (((((((𝜑𝑢𝐽) ∧ 𝑣𝐽) ∧ (𝑢 𝑘𝐴𝐵) ≠ ∅) ∧ (𝑣 𝑘𝐴𝐵) ≠ ∅) ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)) ∧ 𝑘𝐴𝐵 ⊆ (𝑢𝑣)) ↔ (   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   ,   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   ,    𝑘𝐴𝐵 ⊆ (𝑢𝑣)   ))
qed1,2,3,4,5 (   𝜑   ▶   (𝐽t 𝑘𝐴𝐵) ∈ Con   )