Theorem iunconlem2VD

Description: The indexed union of connected overlapping subspaces sharing a common point is connected. The Virtual Deduction form of the proof is iunconlem2VD. The Metamath form of the proof is iunconlem2. The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of iuncon. The Virtual Deduction proof is verified by automatically transforming it into the Metamath form of the proof using completeusersproof, which is verified by the Metamath program. The proof of iunconlem2RO is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. iunconlem2VD differs from iuncon only in that it is in Virtual Deduction notation and iuncon does not have the first hypothesis of iunconlem2VD, which is eliminated in iunconALT. (Contributed by Alan Sare, 5-Apr-2018.)

Hypotheses

Ref	Expression
iunconlem2VD.1	⊢ (𝜓 ↔ (   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅   ,   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵)   ,   ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)   ))
iunconlem2VD.2	⊢ (   𝜑   ▶   𝐽 ∈ (TopOn‘𝑋)   )
iunconlem2VD.3	⊢ (   (   𝜑   ,   𝑘 ∈ 𝐴   )   ▶   𝐵 ⊆ 𝑋   )
iunconlem2VD.4	⊢ (   (   𝜑   ,   𝑘 ∈ 𝐴   )   ▶   𝑃 ∈ 𝐵   )
iunconlem2VD.5	⊢ (   (   𝜑   ,   𝑘 ∈ 𝐴   )   ▶   (𝐽 ↾t 𝐵) ∈ Con   )

Assertion

Ref	Expression
iunconlem2VD	⊢ (   𝜑   ▶   (𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Con   )

Distinct variable groups:   𝑢,𝑘,𝑣,𝜑   𝐴,𝑘,𝑢,𝑣   𝑢,𝐵,𝑣   𝑘,𝐽,𝑢,𝑣   𝑃,𝑘   𝑘,𝑋,𝑢,𝑣 Allowed substitution hints:   𝜓(𝑣,𝑢,𝑘)   𝐵(𝑘)   𝑃(𝑣,𝑢)

Proof of Theorem iunconlem2VD

		⊢
⊢
Proof of lemma1
⊢ Ⅎ𝑘(   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   ,   ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)   )
Step	Hyp	Expression
1		⊢ Ⅎ𝑘(   𝜑   ,   𝑢 ∈ 𝐽   )
2		⊢ Ⅎ𝑘𝑣 ∈ 𝐽
3	1, 2	⊢ Ⅎ𝑘((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐽)
4		⊢ Ⅎ𝑘𝑢
5		⊢ Ⅎ𝑘∪ 𝑘 ∈ 𝐴𝐵
6	4, 5	⊢ Ⅎ𝑘(𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵)
7		⊢ Ⅎ𝑘∅
8	6, 7	⊢ Ⅎ𝑘(𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅
9	3, 8	⊢ Ⅎ𝑘(   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   )
10		⊢ Ⅎ𝑘𝑣
11	10, 5	⊢ Ⅎ𝑘(𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵)
12	11, 7	⊢ Ⅎ𝑘(𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅
13	9, 12	⊢ Ⅎ𝑘(   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   )
14		⊢ Ⅎ𝑘(𝑢 ∩ 𝑣)
15		⊢ Ⅎ𝑘𝑋
16	15, 5	⊢ Ⅎ𝑘(𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)
17	14, 16	⊢ Ⅎ𝑘(𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)
18	13, 17	⊢ Ⅎ𝑘(   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   )
19		⊢ Ⅎ𝑘(𝑢 ∪ 𝑣)
20	5, 19	⊢ Ⅎ𝑘∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)
lemma1	18, 20	⊢ Ⅎ𝑘(   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   ,   ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)   )
⊢
Proof of iunconlem2VD
⊢ (   𝜑   ▶   (𝐽 ↾t ∪ 𝑘 ∈ 𝐴𝐵) ∈ Con   )
Step	Hyp	Expression
h22		⊢ (𝜓 ↔ (   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   ,   ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)   ))
23	22	⊢ (Ⅎ𝑘𝜓 ↔ Ⅎ𝑘(   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   ,   ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)   ))
24	lemma1, 23	⊢ Ⅎ𝑘𝜓
25	22	⊢ (   𝜓   ▶   (   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   ,   ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)   )   )
26	25	⊢ (   𝜓   ▶   𝜑   )
h27		⊢ (   𝜑   ▶   𝐽 ∈ (TopOn‘𝑋)   )
28	26, 27	⊢ (   𝜓   ▶   𝐽 ∈ (TopOn‘𝑋)   )
h29		⊢ (   (   𝜑   ,   𝑘 ∈ 𝐴   )   ▶   𝐵 ⊆ 𝑋   )
30	26, 29	⊢ (   (   𝜓   ,   𝑘 ∈ 𝐴   )   ▶   𝐵 ⊆ 𝑋   )
h31		⊢ (   (   𝜑   ,   𝑘 ∈ 𝐴   )   ▶   𝑃 ∈ 𝐵   )
32	26, 31	⊢ (   (   𝜓   ,   𝑘 ∈ 𝐴   )   ▶   𝑃 ∈ 𝐵   )
33	32	⊢ (   𝜓   ▶   (𝑘 ∈ 𝐴 → 𝑃 ∈ 𝐵)   )
h34		⊢ (   (   𝜑   ,   𝑘 ∈ 𝐴   )   ▶   (𝐽 ↾t 𝐵) ∈ Con   )
35	26, 34	⊢ (   (   𝜓   ,   𝑘 ∈ 𝐴   )   ▶   (𝐽 ↾t 𝐵) ∈ Con   )
36	25	⊢ (   𝜓   ▶   𝑢 ∈ 𝐽   )
37	25	⊢ (   𝜓   ▶   𝑣 ∈ 𝐽   )
38	25	⊢ (   𝜓   ▶   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   )
39	25	⊢ (   𝜓   ▶   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   )
40	25	⊢ (   𝜓   ▶   ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)   )
41	28, 30, 32, 35, 36, 37, 38, 39, 40, 24	⊢ (   𝜓   ▶   ¬ 𝑃 ∈ 𝑢   )
42		⊢ (𝑣 ∩ 𝑢) = (𝑢 ∩ 𝑣)
43	39, 42	⊢ (   𝜓   ▶   (𝑣 ∩ 𝑢) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   )
44		⊢ (𝑣 ∪ 𝑢) = (𝑢 ∪ 𝑣)
45	40, 44	⊢ (   𝜓   ▶   ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑣 ∪ 𝑢)   )
46	25	⊢ (   𝜓   ▶   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   )
47	28, 30, 32, 35, 37, 36, 46, 43, 45, 24	⊢ (   𝜓   ▶   ¬ 𝑃 ∈ 𝑣   )
48	41, 47	⊢ (   𝜓   ▶   ¬ (𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣)   )
49		⊢ (   𝑤 ∈ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵)   ▶   𝑤 ∈ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵)   )
50		⊢ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ⊆ ∪ 𝑘 ∈ 𝐴𝐵
51	49, 50	⊢ (   𝑤 ∈ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵)   ▶   𝑤 ∈ ∪ 𝑘 ∈ 𝐴𝐵   )
52	51	⊢ (   𝑤 ∈ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵)   ▶   ∃𝑘 ∈ 𝐴𝑤 ∈ 𝐵   )
53	52	⊢ (   𝑤 ∈ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵)   ▶   𝐴 ≠ ∅   )
54	53	⊢ (∃𝑤𝑤 ∈ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) → 𝐴 ≠ ∅)
55	46	⊢ (   𝜓   ▶   ∃𝑤𝑤 ∈ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵)   )
56	55, 54	⊢ (   𝜓   ▶   𝐴 ≠ ∅   )
57	24, 33	⊢ (   𝜓   ▶   ∀𝑘 ∈ 𝐴𝑃 ∈ 𝐵   )
58	56, 57	⊢ (   𝜓   ▶   ∃𝑘 ∈ 𝐴𝑃 ∈ 𝐵   )
59	58	⊢ (   𝜓   ▶   𝑃 ∈ ∪ 𝑘 ∈ 𝐴𝐵   )
60	59, 40	⊢ (   𝜓   ▶   𝑃 ∈ (𝑢 ∪ 𝑣)   )
61	60	⊢ (   𝜓   ▶   (𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣)   )
62	48, 22	⊢ (   (   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   ,   ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)   )   ▶   ¬ (𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣)   )
63	61, 22	⊢ (   (   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   ,   ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)   )   ▶   (𝑃 ∈ 𝑢 ∨ 𝑃 ∈ 𝑣)   )
64	62, 63	⊢ (   (   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)   )   ▶   ¬ ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)   )
65	64	⊢ (   (   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   ,   (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   )   ▶   ((𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵) → ¬ ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣))   )
66	65	⊢ (   (   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   ,   (𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅   )   ▶   ((𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ → ((𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵) → ¬ ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)))   )
67	66	⊢ (   (   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   )   ▶   ((𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ → ((𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ → ((𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵) → ¬ ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣))))   )
68	67	⊢ (   (   𝜑   ,   𝑢 ∈ 𝐽   ,   𝑣 ∈ 𝐽   )   ▶   (((𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)) → ¬ ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣))   )
69	68	⊢ (   (   𝜑   ,   𝑢 ∈ 𝐽   )   ▶   (𝑣 ∈ 𝐽 → (((𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)) → ¬ ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)))   )
70	69	⊢ (   𝜑   ▶   (𝑢 ∈ 𝐽 → (𝑣 ∈ 𝐽 → (((𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)) → ¬ ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣))))   )
71	70	⊢ (   𝜑   ▶   ((𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽) → (((𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)) → ¬ ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣)))   )
72	71	⊢ (   𝜑   ▶   ∀𝑢 ∈ 𝐽∀𝑣 ∈ 𝐽(((𝑢 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ ∧ (𝑣 ∩ ∪ 𝑘 ∈ 𝐴𝐵) ≠ ∅ ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴𝐵)) → ¬ ∪ 𝑘 ∈ 𝐴𝐵 ⊆ (𝑢 ∪ 𝑣))   )
73	29	⊢ (   𝜑   ▶   (𝑘 ∈ 𝐴 → 𝐵 ⊆ 𝑋)   )
74	73	⊢ (   𝜑   ▶   ∀𝑘 ∈ 𝐴𝐵 ⊆ 𝑋   )
75	74	⊢ (   𝜑   ▶   ∪ 𝑘 ∈ 𝐴𝐵 ⊆ 𝑋   )
qed	27, 75, 72	⊢ (   𝜑   ▶   (𝐽 ↾t ∪ 𝑘 ∈ 𝐴𝐵) ∈ Con   )