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
𝑘(   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   ,   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   ,    𝑘𝐴𝐵 ⊆ (𝑢𝑣)   )
StepHypExpression
1  𝑘(   𝜑   ,   𝑢𝐽   )
2  𝑘𝑣𝐽
31, 2 𝑘((𝜑𝑢𝐽) ∧ 𝑣𝐽)
4  𝑘𝑢
5  𝑘 𝑘𝐴𝐵
64, 5 𝑘(𝑢 𝑘𝐴𝐵)
7  𝑘
86, 7 𝑘(𝑢 𝑘𝐴𝐵) ≠ ∅
93, 8 𝑘(   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   )
10  𝑘𝑣
1110, 5 𝑘(𝑣 𝑘𝐴𝐵)
1211, 7 𝑘(𝑣 𝑘𝐴𝐵) ≠ ∅
139, 12 𝑘(   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   )
14  𝑘(𝑢𝑣)
15  𝑘𝑋
1615, 5 𝑘(𝑋 𝑘𝐴𝐵)
1714, 16 𝑘(𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)
1813, 17 𝑘(   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   ,   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   )
19  𝑘(𝑢𝑣)
205, 19 𝑘 𝑘𝐴𝐵 ⊆ (𝑢𝑣)
lemma118, 20 𝑘(   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   ,   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   ,    𝑘𝐴𝐵 ⊆ (𝑢𝑣)   )
Proof of iunconlem2VD
(   𝜑   ▶   (𝐽t 𝑘𝐴𝐵) ∈ Con   )
StepHypExpression
h22  (𝜓(   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   ,   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   ,    𝑘𝐴𝐵 ⊆ (𝑢𝑣)   ))
2322 (Ⅎ𝑘𝜓 ↔ Ⅎ𝑘(   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   ,   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   ,    𝑘𝐴𝐵 ⊆ (𝑢𝑣)   ))
24lemma1, 23 𝑘𝜓
2522 (   𝜓   ▶   (   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   ,   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   ,    𝑘𝐴𝐵 ⊆ (𝑢𝑣)   )   )
2625 (   𝜓   ▶   𝜑   )
h27  (   𝜑   ▶   𝐽 ∈ (TopOn‘𝑋)   )
2826, 27 (   𝜓   ▶   𝐽 ∈ (TopOn‘𝑋)   )
h29  (   (   𝜑   ,   𝑘𝐴   )   ▶   𝐵𝑋   )
3026, 29 (   (   𝜓   ,   𝑘𝐴   )   ▶   𝐵𝑋   )
h31  (   (   𝜑   ,   𝑘𝐴   )   ▶   𝑃𝐵   )
3226, 31 (   (   𝜓   ,   𝑘𝐴   )   ▶   𝑃𝐵   )
3332 (   𝜓   ▶   (𝑘𝐴𝑃𝐵)   )
h34  (   (   𝜑   ,   𝑘𝐴   )   ▶   (𝐽t 𝐵) ∈ Con   )
3526, 34 (   (   𝜓   ,   𝑘𝐴   )   ▶   (𝐽t 𝐵) ∈ Con   )
3625 (   𝜓   ▶   𝑢𝐽   )
3725 (   𝜓   ▶   𝑣𝐽   )
3825 (   𝜓   ▶   (𝑣 𝑘𝐴𝐵) ≠ ∅   )
3925 (   𝜓   ▶   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   )
4025 (   𝜓   ▶    𝑘𝐴𝐵 ⊆ (𝑢𝑣)   )
4128, 30, 32, 35, 36, 37, 38, 39, 40, 24 (   𝜓   ▶   ¬ 𝑃𝑢   )
42  (𝑣𝑢) = (𝑢𝑣)
4339, 42 (   𝜓   ▶   (𝑣𝑢) ⊆ (𝑋 𝑘𝐴𝐵)   )
44  (𝑣𝑢) = (𝑢𝑣)
4540, 44 (   𝜓   ▶    𝑘𝐴𝐵 ⊆ (𝑣𝑢)   )
4625 (   𝜓   ▶   (𝑢 𝑘𝐴𝐵) ≠ ∅   )
4728, 30, 32, 35, 37, 36, 46, 43, 45, 24 (   𝜓   ▶   ¬ 𝑃𝑣   )
4841, 47 (   𝜓   ▶   ¬ (𝑃𝑢𝑃𝑣)   )
49  (   𝑤 ∈ (𝑢 𝑘𝐴𝐵)   ▶   𝑤 ∈ (𝑢 𝑘𝐴𝐵)   )
50  (𝑢 𝑘𝐴𝐵) ⊆ 𝑘𝐴𝐵
5149, 50 (   𝑤 ∈ (𝑢 𝑘𝐴𝐵)   ▶   𝑤 𝑘𝐴𝐵   )
5251 (   𝑤 ∈ (𝑢 𝑘𝐴𝐵)   ▶   𝑘𝐴𝑤𝐵   )
5352 (   𝑤 ∈ (𝑢 𝑘𝐴𝐵)   ▶   𝐴 ≠ ∅   )
5453 (∃𝑤𝑤 ∈ (𝑢 𝑘𝐴𝐵) → 𝐴 ≠ ∅)
5546 (   𝜓   ▶   𝑤𝑤 ∈ (𝑢 𝑘𝐴𝐵)   )
5655, 54 (   𝜓   ▶   𝐴 ≠ ∅   )
5724, 33 (   𝜓   ▶   𝑘𝐴𝑃𝐵   )
5856, 57 (   𝜓   ▶   𝑘𝐴𝑃𝐵   )
5958 (   𝜓   ▶   𝑃 𝑘𝐴𝐵   )
6059, 40 (   𝜓   ▶   𝑃 ∈ (𝑢𝑣)   )
6160 (   𝜓   ▶   (𝑃𝑢𝑃𝑣)   )
6248, 22 (   (   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   ,   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   ,    𝑘𝐴𝐵 ⊆ (𝑢𝑣)   )   ▶   ¬ (𝑃𝑢𝑃𝑣)   )
6361, 22 (   (   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   ,   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   ,    𝑘𝐴𝐵 ⊆ (𝑢𝑣)   )   ▶   (𝑃𝑢𝑃𝑣)   )
6462, 63 (   (   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   ,   (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)   )   ▶   ¬ 𝑘𝐴𝐵 ⊆ (𝑢𝑣)   )
6564 (   (   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   ,   (𝑣 𝑘𝐴𝐵) ≠ ∅   )   ▶   ((𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵) → ¬ 𝑘𝐴𝐵 ⊆ (𝑢𝑣))   )
6665 (   (   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   ,   (𝑢 𝑘𝐴𝐵) ≠ ∅   )   ▶   ((𝑣 𝑘𝐴𝐵) ≠ ∅ → ((𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵) → ¬ 𝑘𝐴𝐵 ⊆ (𝑢𝑣)))   )
6766 (   (   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   )   ▶   ((𝑢 𝑘𝐴𝐵) ≠ ∅ → ((𝑣 𝑘𝐴𝐵) ≠ ∅ → ((𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵) → ¬ 𝑘𝐴𝐵 ⊆ (𝑢𝑣))))   )
6867 (   (   𝜑   ,   𝑢𝐽   ,   𝑣𝐽   )   ▶   (((𝑢 𝑘𝐴𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)) → ¬ 𝑘𝐴𝐵 ⊆ (𝑢𝑣))   )
6968 (   (   𝜑   ,   𝑢𝐽   )   ▶   (𝑣𝐽 → (((𝑢 𝑘𝐴𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)) → ¬ 𝑘𝐴𝐵 ⊆ (𝑢𝑣)))   )
7069 (   𝜑   ▶   (𝑢𝐽 → (𝑣𝐽 → (((𝑢 𝑘𝐴𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)) → ¬ 𝑘𝐴𝐵 ⊆ (𝑢𝑣))))   )
7170 (   𝜑   ▶   ((𝑢𝐽𝑣𝐽) → (((𝑢 𝑘𝐴𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)) → ¬ 𝑘𝐴𝐵 ⊆ (𝑢𝑣)))   )
7271 (   𝜑   ▶   𝑢𝐽𝑣𝐽(((𝑢 𝑘𝐴𝐵) ≠ ∅ ∧ (𝑣 𝑘𝐴𝐵) ≠ ∅ ∧ (𝑢𝑣) ⊆ (𝑋 𝑘𝐴𝐵)) → ¬ 𝑘𝐴𝐵 ⊆ (𝑢𝑣))   )
7329 (   𝜑   ▶   (𝑘𝐴𝐵𝑋)   )
7473 (   𝜑   ▶   𝑘𝐴𝐵𝑋   )
7574 (   𝜑   ▶    𝑘𝐴𝐵𝑋   )
qed27, 75, 72 (   𝜑   ▶   (𝐽t 𝑘𝐴𝐵) ∈ Con   )
  Copyright terms: Public domain W3C validator