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