Theorem iunconnALT

Description: The indexed union of connected overlapping subspaces sharing a common point is connected. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/iunconaltvd.html . As it is verified by the Metamath program, iunconnALT verifies https://us.metamath.org/other/completeusersproof/iunconaltvd.html . (Contributed by Alan Sare, 22-Apr-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	iunconnALT.1	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	iunconnALT.2	$$⊢\left(\phi \wedge k\in A\right)\to B\subseteq X$$
	iunconnALT.3	$$⊢\left(\phi \wedge k\in A\right)\to P\in B$$
	iunconnALT.4	$$⊢\left(\phi \wedge k\in A\right)\to J{\upharpoonright }_{𝑡}B\in \mathrm{Conn}$$
Assertion	iunconnALT	$$⊢\phi \to J{\upharpoonright }_{𝑡}\bigcup _{k\in A}B\in \mathrm{Conn}$$

Proof

Step	Hyp	Ref	Expression
1		iunconnALT.1	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
2		iunconnALT.2	$$⊢\left(\phi \wedge k\in A\right)\to B\subseteq X$$
3		iunconnALT.3	$$⊢\left(\phi \wedge k\in A\right)\to P\in B$$
4		iunconnALT.4	$$⊢\left(\phi \wedge k\in A\right)\to J{\upharpoonright }_{𝑡}B\in \mathrm{Conn}$$
5		biid	$$⊢\left(\left(\left(\left(\left(\left(\phi \wedge u\in J\right)\wedge v\in J\right)\wedge u\cap \bigcup _{k\in A}B\ne \varnothing \right)\wedge v\cap \bigcup _{k\in A}B\ne \varnothing \right)\wedge u\cap v\subseteq X\setminus \bigcup _{k\in A}B\right)\wedge \bigcup _{k\in A}B\subseteq u\cup v\right)\leftrightarrow \left(\left(\left(\left(\left(\left(\phi \wedge u\in J\right)\wedge v\in J\right)\wedge u\cap \bigcup _{k\in A}B\ne \varnothing \right)\wedge v\cap \bigcup _{k\in A}B\ne \varnothing \right)\wedge u\cap v\subseteq X\setminus \bigcup _{k\in A}B\right)\wedge \bigcup _{k\in A}B\subseteq u\cup v\right)$$
6	5 1 2 3 4	iunconnlem2	$$⊢\phi \to J{\upharpoonright }_{𝑡}\bigcup _{k\in A}B\in \mathrm{Conn}$$