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 | ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) | |
| iunconnALT.2 | ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 ) | ||
| iunconnALT.3 | ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 ) | ||
| iunconnALT.4 | ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn ) | ||
| Assertion | iunconnALT | ⊢ ( 𝜑 → ( 𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵 ) ∈ Conn ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iunconnALT.1 | ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) | |
| 2 | iunconnALT.2 | ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ 𝑋 ) | |
| 3 | iunconnALT.3 | ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 ) | |
| 4 | iunconnALT.4 | ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐽 ↾t 𝐵 ) ∈ Conn ) | |
| 5 | biid | ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ↔ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵 ) ≠ ∅ ) ∧ ( 𝑢 ∩ 𝑣 ) ⊆ ( 𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵 ) ) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ ( 𝑢 ∪ 𝑣 ) ) ) | |
| 6 | 5 1 2 3 4 | iunconnlem2 | ⊢ ( 𝜑 → ( 𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵 ) ∈ Conn ) |