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   )
Copyright terms: Public domain