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 )
|
|