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	|- ( ph -> J e. ( TopOn ` X ) )
	iunconnALT.2	|- ( ( ph /\ k e. A ) -> B C_ X )
	iunconnALT.3	|- ( ( ph /\ k e. A ) -> P e. B )
	iunconnALT.4	|- ( ( ph /\ k e. A ) -> ( J |`t B ) e. Conn )
Assertion	iunconnALT	|- ( ph -> ( J |`t U_ k e. A B ) e. Conn )

Proof

Step	Hyp	Ref	Expression
1		iunconnALT.1	|- ( ph -> J e. ( TopOn ` X ) )
2		iunconnALT.2	|- ( ( ph /\ k e. A ) -> B C_ X )
3		iunconnALT.3	|- ( ( ph /\ k e. A ) -> P e. B )
4		iunconnALT.4	|- ( ( ph /\ k e. A ) -> ( J |`t B ) e. Conn )
5		biid	|- ( ( ( ( ( ( ( ph /\ u e. J ) /\ v e. J ) /\ ( u i^i U_ k e. A B ) =/= (/) ) /\ ( v i^i U_ k e. A B ) =/= (/) ) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) /\ U_ k e. A B C_ ( u u. v ) ) <-> ( ( ( ( ( ( ph /\ u e. J ) /\ v e. J ) /\ ( u i^i U_ k e. A B ) =/= (/) ) /\ ( v i^i U_ k e. A B ) =/= (/) ) /\ ( u i^i v ) C_ ( X \ U_ k e. A B ) ) /\ U_ k e. A B C_ ( u u. v ) ) )
6	5 1 2 3 4	iunconnlem2	|- ( ph -> ( J |`t U_ k e. A B ) e. Conn )